let s1, s2 be State of ; :: thesis: for I being Program of st DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1 holds
I is_pseudo-closed_on s2
set D = Int-Locations \/ FinSeq-Locations ;
let I be Program of ; :: thesis: ( DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1 implies I is_pseudo-closed_on s2 )
set S1 = s1 +* (I +* (Start-At (insloc 0 )));
set S2 = s2 +* (I +* (Start-At (insloc 0 )));
A1: I +* (Start-At (insloc 0 )) c= s1 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
A2: IC (s2 +* (I +* (Start-At (insloc 0 )))) = IC ((s2 +* I) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= insloc 0 by AMI_1:111 ;
A3: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
I +* (Start-At (insloc 0 )) c= s2 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then I c= s2 +* (I +* (Start-At (insloc 0 ))) by A3, XBOOLE_1:1;
then A4: ProgramPart (Relocated I,0 ) c= s2 +* (I +* (Start-At (insloc 0 ))) by Th9;
assume DataPart s1 = DataPart s2 ; :: thesis: ( not I is_pseudo-closed_on s1 or I is_pseudo-closed_on s2 )
then A5: DataPart (s1 +* (I +* (Start-At (insloc 0 )))) = DataPart s2 by SCMFSA8A:11
.= DataPart (s2 +* (I +* (Start-At (insloc 0 )))) by SCMFSA8A:11 ;
assume A6: I is_pseudo-closed_on s1 ; :: thesis: I is_pseudo-closed_on s2
then A7: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s1,I)) = insloc (card (ProgramPart I)) by SCMFSA8A:def 5;
A8: I is_pseudo-closed_on s1 +* (I +* (Start-At (insloc 0 ))) by A6, Th50;

A9: now

let k be Element of NAT ; :: thesis: ( k < pseudo-LifeSpan s1,I implies IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I )
assume A10: k < pseudo-LifeSpan s1,I ; :: thesis: IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I
then k <= pseudo-LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))),I by A6, Th50;
then IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) = (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)) + 0 by A5, A8, A1, A4, A2, Th51
.= IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) ;
hence IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A6, A10, SCMFSA8A:def 5; :: thesis: verum

end;

IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s1,I)) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))),I)) by A6, Th50
.= (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))),I))) + 0 by A5, A8, A1, A4, A2, Th51
.= IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s1,I)) by A6, Th50 ;
hence I is_pseudo-closed_on s2 by A7, A9, SCMFSA8A:def 3; :: thesis: verum