deffunc H_{1}( 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 = H_{1}(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

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

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 = H

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

then reconsider F = F as Function-yielding FinSequence ;
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;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

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