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