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