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;

( 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

hence
f1 = f2
by A6, A7, A9, A10, A12, A13, A14, FINSEQ_1:13; :: thesis: verumF1 . 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;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