let s1, s2 be State of SCM+FSA; :: thesis: for p1, p2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being InitHalting Program of SCM+FSA st Initialized I c= s1 & Initialized I c= s2 & I c= p1 & I c= p2 & s1,s2 equal_outside NAT holds
( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1), Result (p2,s2) equal_outside NAT )
let p1, p2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being InitHalting Program of SCM+FSA st Initialized I c= s1 & Initialized I c= s2 & I c= p1 & I c= p2 & s1,s2 equal_outside NAT holds
( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1), Result (p2,s2) equal_outside NAT )
let I be InitHalting Program of SCM+FSA; :: thesis: ( Initialized I c= s1 & Initialized I c= s2 & I c= p1 & I c= p2 & s1,s2 equal_outside NAT implies ( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1), Result (p2,s2) equal_outside NAT ) )
assume that
A1: Initialized I c= s1 and
A2: Initialized I c= s2 and
A3: I c= p1 and
A4: I c= p2 and
A5: s1,s2 equal_outside NAT ; :: thesis: ( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1), Result (p2,s2) equal_outside NAT )
A6: p2 halts_on s2 by A2, Th5, A4;
A7: p1 halts_on s1 by A1, Th5, A3;

A8: now

let l be Element of NAT ; :: thesis: ( CurInstr (p2,(Comput (p2,s2,l))) = halt SCM+FSA implies LifeSpan (p1,s1) <= l )
assume A9: CurInstr (p2,(Comput (p2,s2,l))) = halt SCM+FSA ; :: thesis: LifeSpan (p1,s1) <= l
CurInstr (p1,(Comput (p1,s1,l))) = CurInstr (p2,(Comput (p2,s2,l))) by A1, A2, A5, Th14, A3, A4;
hence LifeSpan (p1,s1) <= l by A7, A9, EXTPRO_1:def 14; :: thesis: verum

end;

CurInstr (p2,(Comput (p2,s2,(LifeSpan (p1,s1))))) = CurInstr (p1,(Comput (p1,s1,(LifeSpan (p1,s1))))) by A1, A2, A5, Th14, A3, A4
.= halt SCM+FSA by A7, EXTPRO_1:def 14 ;
hence A10: LifeSpan (p1,s1) = LifeSpan (p2,s2) by A8, A6, EXTPRO_1:def 14; :: thesis: Result (p1,s1), Result (p2,s2) equal_outside NAT
A11: Result (p2,s2) = Comput (p2,s2,(LifeSpan (p1,s1))) by A10, A2, Th5, EXTPRO_1:23, A4;
Result (p1,s1) = Comput (p1,s1,(LifeSpan (p1,s1))) by A1, Th5, EXTPRO_1:23, A3;
hence Result (p1,s1), Result (p2,s2) equal_outside NAT by A1, A2, A5, A11, Th14, A3, A4; :: thesis: verum