[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] 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