Re: a question about a proof and a method

Dear Adem,

you have no chance to prove the existence of the definition

> definition
>  let o be real number, fs be FinSequence;
>  assume TAS: 1 <= len fs;
>  func distr(o,fs) -> FinSequence means
>    dom it = Seg(len fs) &
>    it.1 = S &
>    for i being Nat st i in Seg(len fs)\{1} holds
>      ex p being FinSequence st p = fs.i & it.i = sexp(o,p);

The problem is that loci 'fs' must be 'FinSequence-yielding' to ensure 
that 'fs.i' is a FinSequence.


Look at:

definition
   let IT be Function;
   attr IT is FinSequence-yielding means
:: PRE_POLY:def 3
   for x st x in dom IT holds IT.x is FinSequence;
end;

Best
Artur