set D = Int-Locations \/ FinSeq-Locations ;
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 holds
I is_pseudo-closed_on s2
let I be Program of SCM+FSA ; :: 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 )));
assume DataPart s1 = DataPart s2 ; :: thesis: ( not I is_pseudo-closed_on s1 or I is_pseudo-closed_on s2 )
then A1: DataPart (s1 +* (I +* (Start-At (insloc 0 )))) = DataPart s2 by SCMFSA8A:11
.= DataPart (s2 +* (I +* (Start-At (insloc 0 )))) by SCMFSA8A:11 ;
assume A2: I is_pseudo-closed_on s1 ; :: thesis: I is_pseudo-closed_on s2
then A3: ( IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s1,I)) = insloc (card (ProgramPart I)) & ( for n being Element of NAT st n < pseudo-LifeSpan s1,I holds
IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),n) in dom I ) ) by SCMFSA8A:def 5;
A4: I is_pseudo-closed_on s1 +* (I +* (Start-At (insloc 0 ))) by A2, Th50;
A5: I +* (Start-At (insloc 0 )) c= s1 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
A6: I +* (Start-At (insloc 0 )) c= s2 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then I c= s2 +* (I +* (Start-At (insloc 0 ))) by A6, XBOOLE_1:1;
then A7: ProgramPart (Relocated I,0 ) c= s2 +* (I +* (Start-At (insloc 0 ))) by Th9;
A8: IC (s2 +* (I +* (Start-At (insloc 0 )))) = IC ((s2 +* I) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= insloc 0 by AMI_1:111 ;
A9: 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 A2, Th50
.= (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))),I))) + 0 by A1, A4, A5, A7, A8, Th51
.= IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s1,I)) by A2, Th50 ;

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 A2, Th50;
then IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) = (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)) + 0 by A1, A4, A5, A7, A8, Th51
.= IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) ;
hence IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A2, A10, SCMFSA8A:def 5; :: thesis: verum

end;

hence I is_pseudo-closed_on s2 by A3, A9, SCMFSA8A:def 3; :: thesis: verum