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) = H1(i,F1 . i) and
A5: F2 . 0 = s and
A6: for i being Nat holds F2 . (i + 1) = H1(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) = H2(i,F1 . i) by A4;
A9: F2 . 0 = s by A5;
A10: for i being Nat holds F2 . (i + 1) = H2(i,F2 . i) by A6;
F1 = F2 from NAT_1:sch 16(A7, A8, A9, A10);
 hence F1 = F2 ; :: thesis: verum