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 AMI_1:111 ;
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