let s1, s2 be State of SCM+FSA ; :: thesis: for I, J being Program of SCM+FSA st DataPart s1 = DataPart s2 holds
s1 +* (I +* (Start-At 0 ,SCM+FSA )),s2 +* (J +* (Start-At 0 ,SCM+FSA )) equal_outside NAT
let I, J be Program of SCM+FSA ; :: thesis: ( DataPart s1 = DataPart s2 implies s1 +* (I +* (Start-At 0 ,SCM+FSA )),s2 +* (J +* (Start-At 0 ,SCM+FSA )) equal_outside NAT )
assume A1: DataPart s1 = DataPart s2 ; :: thesis: s1 +* (I +* (Start-At 0 ,SCM+FSA )),s2 +* (J +* (Start-At 0 ,SCM+FSA )) equal_outside NAT
set S2 = s2 +* (J +* (Start-At 0 ,SCM+FSA ));
set S1 = s1 +* (I +* (Start-At 0 ,SCM+FSA ));
A2: IC (s1 +* (I +* (Start-At 0 ,SCM+FSA ))) = 0 by FUNCT_4:26, SF_MASTR:67;
A3: IC (s2 +* (J +* (Start-At 0 ,SCM+FSA ))) = 0 by FUNCT_4:26, SF_MASTR:67;
DataPart (s1 +* (I +* (Start-At 0 ,SCM+FSA ))) = DataPart s1 by SCMFSA8A:11
.= DataPart (s2 +* (J +* (Start-At 0 ,SCM+FSA ))) by A1, SCMFSA8A:11 ;
hence s1 +* (I +* (Start-At 0 ,SCM+FSA )),s2 +* (J +* (Start-At 0 ,SCM+FSA )) equal_outside NAT by A2, A3, SCMFSA8A:6; :: thesis: verum