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 ((ProgramPart ((F1 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((F1 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ((F1 . i) +* (I +* (Start-At (0,SCM+FSA))))),((F1 . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 3)) ) & F2 . 0 = s & ( for i being Nat holds F2 . (i + 1) = Comput ((ProgramPart ((F2 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((F2 . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart ((F2 . i) +* (I +* (Start-At (0,SCM+FSA))))),((F2 . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 3)) ) implies F1 = F2 )
assume that
B1: F1 . 0 = s and
B2: for i being Nat holds F1 . (i + 1) = H₁(i,F1 . i) and
B3: F2 . 0 = s and
B4: for i being Nat holds F2 . (i + 1) = H₁(i,F2 . i) ; :: thesis: F1 = F2
reconsider s = s as Element of product the Object-Kind of SCM+FSA by PBOOLE:155;
A1: F1 . 0 = s by B1;
A2: for i being Nat holds F1 . (i + 1) = H₂(i,F1 . i) by B2;
A3: F2 . 0 = s by B3;
A4: for i being Nat holds F2 . (i + 1) = H₂(i,F2 . i) by B4;
F1 = F2 from NAT_1:sch 16(A1, A2, A3, A4);
hence F1 = F2 ; :: thesis: verum