let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
LifeSpan (P1,s1) = LifeSpan (P2,s2)
let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
LifeSpan (P1,s1) = LifeSpan (P2,s2)
let J be Program of SCM+FSA; :: thesis: ( J is_closed_on s1,P1 & J is_halting_on s1,P1 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & J c= P1 & J c= P2 & DataPart s1 = DataPart s2 implies LifeSpan (P1,s1) = LifeSpan (P2,s2) )
assume that
A1: J is_closed_on s1,P1 and
A2: J is_halting_on s1,P1 and
A3: Start-At (0,SCM+FSA) c= s1 and
A4: Start-At (0,SCM+FSA) c= s2 and
A5: J c= P1 and
A6: J c= P2 and
A7: DataPart s1 = DataPart s2 ; :: thesis: LifeSpan (P1,s1) = LifeSpan (P2,s2)
A9: P1 = P1 +* J by A5, FUNCT_4:103, FUNCT_4:104;
s1 = Initialize s1 by A3, FUNCT_4:103, FUNCT_4:104;
then A10: P1 halts_on s1 by A2, A9, SCMFSA7B:def 8;

A11: now

let k be Element of NAT ; :: thesis: ( CurInstr (P2,(Comput (P2,s2,k))) = halt SCM+FSA implies LifeSpan (P1,s1) <= k )
assume CurInstr (P2,(Comput (P2,s2,k))) = halt SCM+FSA ; :: thesis: LifeSpan (P1,s1) <= k
then CurInstr (P1,(Comput (P1,s1,k))) = halt SCM+FSA by A1, A3, A4, A7, Th43, A5, A6;
hence LifeSpan (P1,s1) <= k by A10, EXTPRO_1:def 14; :: thesis: verum

end;

CurInstr (P1,(Comput (P1,s1,(LifeSpan (P1,s1))))) = halt SCM+FSA by A10, EXTPRO_1:def 14;
then A12: CurInstr (P2,(Comput (P2,s2,(LifeSpan (P1,s1))))) = halt SCM+FSA by A1, A3, A4, A7, Th43, A5, A6;
then P2 halts_on s2 by EXTPRO_1:30;
hence LifeSpan (P1,s1) = LifeSpan (P2,s2) by A12, A11, EXTPRO_1:def 14; :: thesis: verum