let F1, F2 be Function of NAT,(product the Object-Kind 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)))) + 3)) ) & 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)))) + 3)) ) 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 Object-Kind 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