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 COMPOS_1:143, FUNCT_4:26;
A3: IC (s2 +* (J +* (Start-At (0,SCM+FSA)))) = 0 by COMPOS_1:143, FUNCT_4:26;
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