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 0 ,SCM+FSA ) c= s1 & I +* (Start-At 0 ,SCM+FSA ) c= s2 & DataPart s1 = DataPart s2 holds
LifeSpan (ProgramPart s1),s1 = LifeSpan (ProgramPart s2),s2
let J be Program of SCM+FSA ; :: thesis: ( J is_closed_on s1 & J is_halting_on s1 & J +* (Start-At 0 ,SCM+FSA ) c= s1 & J +* (Start-At 0 ,SCM+FSA ) c= s2 & DataPart s1 = DataPart s2 implies LifeSpan (ProgramPart s1),s1 = LifeSpan (ProgramPart s2),s2 )
assume that
A1: J is_closed_on s1 and
A2: J is_halting_on s1 and
A3: J +* (Start-At 0 ,SCM+FSA ) c= s1 and
A4: J +* (Start-At 0 ,SCM+FSA ) c= s2 and
A5: DataPart s1 = DataPart s2 ; :: thesis: LifeSpan (ProgramPart s1),s1 = LifeSpan (ProgramPart s2),s2
s1 = s1 +* (J +* (Start-At 0 ,SCM+FSA )) by A3, FUNCT_4:79;
then A6: ProgramPart s1 halts_on s1 by A2, SCMFSA7B:def 8;

A7: now

let k be Element of NAT ; :: thesis: ( CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,k) = halt SCM+FSA implies LifeSpan (ProgramPart s1),s1 <= k )
TX2: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,k) by AMI_1:123;
TX1: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,k) by AMI_1:123;
assume CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,k) = halt SCM+FSA ; :: thesis: LifeSpan (ProgramPart s1),s1 <= k
then CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,k) = halt SCM+FSA by A1, A3, A4, A5, Th43, TX1, TX2;
hence LifeSpan (ProgramPart s1),s1 <= k by A6, AMI_1:def 46; :: thesis: verum

end;

TX1: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1)) by AMI_1:123;
TX2: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) by AMI_1:123;
CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1)) = halt SCM+FSA by A6, AMI_1:def 46;
then A8: CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = halt SCM+FSA by A1, A3, A4, A5, Th43, TX1, TX2;
then ProgramPart s2 halts_on s2 by AMI_1:146;
hence LifeSpan (ProgramPart s1),s1 = LifeSpan (ProgramPart s2),s2 by A8, A7, AMI_1:def 46; :: thesis: verum