let f1, f2 be Function; :: thesis: ( ex F being Function-yielding FinSequence st
( f1 = 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) ) ) & ex F being Function-yielding FinSequence st
( f2 = 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) ) ) implies f1 = f2 )
given F1 being Function-yielding FinSequence such that A6: f1 = compose (F1,(Funcs (P,NAT))) and
A7: len F1 = len C and
A8: for i being Element of NAT st i in dom C holds
F1 . i = fire (C /. i) ; :: thesis: ( for F being Function-yielding FinSequence holds
( not f2 = compose (F,(Funcs (P,NAT))) or not len F = len C or ex i being Element of NAT st
( i in dom C & not F . i = fire (C /. i) ) ) or f1 = f2 )
given F2 being Function-yielding FinSequence such that A9: f2 = compose (F2,(Funcs (P,NAT))) and
A10: len F2 = len C and
A11: for i being Element of NAT st i in dom C holds
F2 . i = fire (C /. i) ; :: thesis: f1 = f2
A12: dom F1 = Seg (len F1) by FINSEQ_1:def 3;
A13: dom F2 = Seg (len F2) by FINSEQ_1:def 3;
A14: dom C = Seg (len C) by FINSEQ_1:def 3;
now :: thesis: for i being Nat st i in dom C holds
F1 . i = F2 . i
let i be Nat; :: thesis: ( i in dom C implies F1 . i = F2 . i )
assume A15: i in dom C ; :: thesis: F1 . i = F2 . i
then F1 . i = fire (C /. i) by A8;
hence F1 . i = F2 . i by A11, A15; :: thesis: verum
end;
hence f1 = f2 by A6, A7, A9, A10, A12, A13, A14, FINSEQ_1:13; :: thesis: verum