let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on s1 & I is_halting_on s1 & I +* (Start-At (insloc 0 )) c= s1 & I +* (Start-At (insloc 0 )) c= s2 & DataPart s1 = DataPart s2 holds
LifeSpan s1 = LifeSpan s2
let J be Program of SCM+FSA ; :: thesis: ( J is_closed_on s1 & J is_halting_on s1 & J +* (Start-At (insloc 0 )) c= s1 & J +* (Start-At (insloc 0 )) c= s2 & DataPart s1 = DataPart s2 implies LifeSpan s1 = LifeSpan s2 )
assume A1: ( J is_closed_on s1 & J is_halting_on s1 & J +* (Start-At (insloc 0 )) c= s1 & J +* (Start-At (insloc 0 )) c= s2 & DataPart s1 = DataPart s2 ) ; :: thesis: LifeSpan s1 = LifeSpan s2
then s1 = s1 +* (J +* (Start-At (insloc 0 ))) by FUNCT_4:79;
then A2: s1 is halting by A1, SCMFSA7B:def 8;
then ( CurInstr (Computation s1,(LifeSpan s1)) = halt SCM+FSA & ( for k being Element of NAT st CurInstr (Computation s1,k) = halt SCM+FSA holds
LifeSpan s1 <= k ) ) by AMI_1:def 46;
then A3: CurInstr (Computation s2,(LifeSpan s1)) = halt SCM+FSA by A1, Th43;
then A4: s2 is halting by AMI_1:def 20;

now

let k be Element of NAT ; :: thesis: ( CurInstr (Computation s2,k) = halt SCM+FSA implies LifeSpan s1 <= k )
assume CurInstr (Computation s2,k) = halt SCM+FSA ; :: thesis: LifeSpan s1 <= k
then CurInstr (Computation s1,k) = halt SCM+FSA by A1, Th43;
hence LifeSpan s1 <= k by A2, AMI_1:def 46; :: thesis: verum

end;

hence LifeSpan s1 = LifeSpan s2 by A3, A4, AMI_1:def 46; :: thesis: verum