deffunc H1( set ) -> Function = fire (C /. $1);
consider F being FinSequence such that
A1: len F = len C and
A2: for k being Nat st k in dom F holds
F . k = H1(k) from FINSEQ_1:sch 2();
 A3: dom F = Seg (len F) by FINSEQ_1:def 3;
A4: dom C = Seg (len C) by FINSEQ_1:def 3;
F is Function-yielding
proof
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 F or x multitude_of is set )
assume A5: x in dom F ; :: thesis: x multitude_of is set
then reconsider i = x as Element of NAT ;
F . x = fire (C /. i) by A2, A5;
hence x multitude_of is set ; :: thesis: verum
end;
then reconsider F = F as Function-yielding FinSequence ;
take f = compose (F,(Funcs (P,NAT))); :: thesis: ex F being Function-yielding FinSequence st
( f = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) )
take F ; :: thesis: ( f = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) )
thus f = compose (F,(Funcs (P,NAT))) ; :: thesis: ( len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) )
thus ( len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) ) by A1, A2, A3, A4; :: thesis: verum