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) & dom F2 = Seg (len F2) & dom C = Seg (len C) ) by FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom C implies F1 . i = F2 . i )
assume A13: i in dom C ; :: thesis: F1 . i = F2 . i
then F1 . i = fire (C /. i) by A8;
hence F1 . i = F2 . i by A11, A13; :: thesis: verum

end;

hence f1 = f2 by A6, A7, A9, A10, A12, FINSEQ_1:17; :: thesis: verum