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 DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 holds
I is_pseudo-closed_on s2,P2
let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 holds
I is_pseudo-closed_on s2,P2
set D = Data-Locations SCM+FSA;
let I be Program of SCM+FSA; :: thesis: ( DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 implies I is_pseudo-closed_on s2,P2 )
set S1 = s1 +* (Initialize I);
set Q1 = P1 +* I;
set S2 = s2 +* (Initialize I);
set Q2 = P2 +* I;
A1: I c= P1 +* I by FUNCT_4:26;
A2: I c= P2 +* I by FUNCT_4:26;
A3: Reloc (I,0) = I by COMPOS_1:157;
A4: Initialize I c= s1 +* (Initialize I) by FUNCT_4:26;
A5: IC (s2 +* (Initialize I)) = IC (Initialize (s2 +* I)) by FUNCT_4:15
.= 0 by FUNCT_4:121 ;
A6: I c= Initialize I by SCMFSA8A:9;
Initialize I c= s2 +* (Initialize I) by FUNCT_4:26;
then I c= s2 +* (Initialize I) by A6, XBOOLE_1:1;
then A7: Reloc (I,0) c= s2 +* (Initialize I) by COMPOS_1:157;
assume DataPart s1 = DataPart s2 ; :: thesis: ( not I is_pseudo-closed_on s1,P1 or I is_pseudo-closed_on s2,P2 )
then A8: DataPart (s1 +* (Initialize I)) = DataPart s2 by SCMFSA8A:11
.= DataPart (s2 +* (Initialize I)) by SCMFSA8A:11 ;
A9: ProgramPart I = I by RELAT_1:209;
assume A10: I is_pseudo-closed_on s1,P1 ; :: thesis: I is_pseudo-closed_on s2,P2
then A11: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(pseudo-LifeSpan (s1,P1,I)))) = card I by SCMFSA8A:def 5, A9;
A12: I is_pseudo-closed_on s1 +* (Initialize I),P1 +* I by A10, Th50;

A13: now

let k be Element of NAT ; :: thesis: ( k < pseudo-LifeSpan (s1,P1,I) implies IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) in dom I )
assume A14: k < pseudo-LifeSpan (s1,P1,I) ; :: thesis: IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) in dom I
then k <= pseudo-LifeSpan ((s1 +* (Initialize I)),(P1 +* I),I) by A10, Th50;
then IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) = (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k))) + 0 by A8, A12, A4, A7, A5, Th51, A1, A2, A3
.= IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) ;
hence IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) in dom I by A10, A14, SCMFSA8A:def 5, A9; :: thesis: verum

end;

IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(pseudo-LifeSpan (s1,P1,I)))) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(pseudo-LifeSpan ((s1 +* (Initialize I)),(P1 +* I),I)))) by A10, Th50
.= (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(pseudo-LifeSpan ((s1 +* (Initialize I)),(P1 +* I),I))))) + 0 by A8, A12, A4, A7, A5, Th51, A1, A2, A3
.= IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(pseudo-LifeSpan (s1,P1,I)))) by A10, Th50 ;
hence I is_pseudo-closed_on s2,P2 by A11, A13, SCMFSA8A:def 3, A9; :: thesis: verum