let F1, F2 be sequence of (product (the_Values_of SCM+FSA)); :: thesis: ( F1 . 0 = s & ( for i being Nat holds F1 . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (F1 . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (F1 . i)))) + 2)) ) & F2 . 0 = s & ( for i being Nat holds F2 . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (F2 . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (F2 . i)))) + 2)) ) implies F1 = F2 )

assume that

A3: F1 . 0 = s and

A4: for i being Nat holds F1 . (i + 1) = H_{1}(i,F1 . i)
and

A5: F2 . 0 = s and

A6: for i being Nat holds F2 . (i + 1) = H_{1}(i,F2 . i)
; :: thesis: F1 = F2

reconsider s = s as Element of product (the_Values_of SCM+FSA) by CARD_3:107;

A7: F1 . 0 = s by A3;

A8: for i being Nat holds F1 . (i + 1) = H_{2}(i,F1 . i)
by A4;

A9: F2 . 0 = s by A5;

A10: for i being Nat holds F2 . (i + 1) = H_{2}(i,F2 . i)
by A6;

F1 = F2 from NAT_1:sch 16(A7, A8, A9, A10);

hence F1 = F2 ; :: thesis: verum

assume that

A3: F1 . 0 = s and

A4: for i being Nat holds F1 . (i + 1) = H

A5: F2 . 0 = s and

A6: for i being Nat holds F2 . (i + 1) = H

reconsider s = s as Element of product (the_Values_of SCM+FSA) by CARD_3:107;

A7: F1 . 0 = s by A3;

A8: for i being Nat holds F1 . (i + 1) = H

A9: F2 . 0 = s by A5;

A10: for i being Nat holds F2 . (i + 1) = H

F1 = F2 from NAT_1:sch 16(A7, A8, A9, A10);

hence F1 = F2 ; :: thesis: verum