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
set D = Int-Locations \/ FinSeq-Locations;
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 (0,SCM+FSA)));
set S2 = s2 +* (I +* (Start-At (0,SCM+FSA)));
A1: I +* (Start-At (0,SCM+FSA)) c= s1 +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
A2: IC (s2 +* (I +* (Start-At (0,SCM+FSA)))) = IC ((s2 +* I) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= 0 by FUNCT_4:121 ;
A3: I c= I +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
I +* (Start-At (0,SCM+FSA)) c= s2 +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then I c= s2 +* (I +* (Start-At (0,SCM+FSA))) by A3, XBOOLE_1:1;
then A4: ProgramPart (Relocated (I,0)) c= s2 +* (I +* (Start-At (0,SCM+FSA))) 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 (0,SCM+FSA)))) = DataPart s2 by SCMFSA8A:11
.= DataPart (s2 +* (I +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11 ;
assume A6: I is_pseudo-closed_on s1 ; :: thesis: I is_pseudo-closed_on s2
then A7: IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (s1,I)))) = card (ProgramPart I) by SCMFSA8A:def 5;
A8: I is_pseudo-closed_on s1 +* (I +* (Start-At (0,SCM+FSA))) by A6, Th50;

A9: now

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

end;

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