let I, J be Program of SCMPDS ; :: thesis: for s being State of SCMPDS holds s +* (Initialized I),s +* (Initialized J) equal_outside NAT
let s be State of SCMPDS ; :: thesis: s +* (Initialized I),s +* (Initialized J) equal_outside NAT
A1: IC SCMPDS in dom (Initialized I) by Th7;

A2: now

let a be Int_position ; :: thesis: (s +* (Initialized J)) . a = (s +* (Initialized I)) . a
A3: not a in dom (Initialized I) by Th31;
not a in dom (Initialized J) by Th31;
hence (s +* (Initialized J)) . a = s . a by FUNCT_4:12
.= (s +* (Initialized I)) . a by A3, FUNCT_4:12 ;
:: thesis: verum

end;

IC SCMPDS in dom (Initialized J) by Th7;
then IC (s +* (Initialized J)) = (Initialized J) . (IC SCMPDS ) by FUNCT_4:14
.= 0 by Th29
.= (Initialized I) . (IC SCMPDS ) by Th29
.= IC (s +* (Initialized I)) by A1, FUNCT_4:14 ;
hence s +* (Initialized I),s +* (Initialized J) equal_outside NAT by A2, Th11; :: thesis: verum