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) = Computation ((F1 . i) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan ((F1 . i) +* (I +* (Start-At (insloc 0 ))))) + 3) ) & F2 . 0 = s & ( for i being Nat holds F2 . (i + 1) = Computation ((F2 . i) +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan ((F2 . i) +* (I +* (Start-At (insloc 0 ))))) + 3) ) implies F1 = F2 )
assume that
A1: F1 . 0 = s and
B1: for i being Nat holds F1 . (i + 1) = H₁(i,F1 . i) and
A2: F2 . 0 = s and
B2: for i being Nat holds F2 . (i + 1) = H₁(i,F2 . i) ; :: thesis: F1 = F2
thus F1 = F2 from NAT_1:sch 16(A1, B1, A2, B2); :: thesis: verum