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 parahalting Program of SCM+FSA st I c= P1 & I c= P2 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & NPP s1 = NPP s2 holds
( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being parahalting Program of SCM+FSA st I c= P1 & I c= P2 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & NPP s1 = NPP s2 holds
( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
let I be parahalting Program of SCM+FSA; :: thesis: ( I c= P1 & I c= P2 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & NPP s1 = NPP s2 implies ( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) ) )
assume that
A1: I c= P1 and
A2: I c= P2 and
A3: Start-At (0,SCM+FSA) c= s1 and
A4: Start-At (0,SCM+FSA) c= s2 and
A5: NPP s1 = NPP s2 ; :: thesis: ( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )
A6: P2 halts_on s2 by A4, Th18, A2;
A7: P1 halts_on s1 by A3, Th18, A1;

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 A3, A4, A5, Th28, A1, A2;
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 A3, A4, A5, Th28, A1, A2
.= 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: NPP (Result (P1,s1)) = NPP (Result (P2,s2))
A11: Result (P2,s2) = Comput (P2,s2,(LifeSpan (P1,s1))) by A10, A4, Th18, A2, EXTPRO_1:23;
Result (P1,s1) = Comput (P1,s1,(LifeSpan (P1,s1))) by A3, Th18, A1, EXTPRO_1:23;
hence NPP (Result (P1,s1)) = NPP (Result (P2,s2)) by A3, A4, A5, A11, Th28, A1, A2; :: thesis: verum