let s be State of SCMPDS ; :: thesis: for I, J being Program of SCMPDS
for l being Element of NAT holds s +* (I +* (Start-At l,SCMPDS )),s +* (J +* (Start-At l,SCMPDS )) equal_outside NAT
let I, J be Program of SCMPDS ; :: thesis: for l being Element of NAT holds s +* (I +* (Start-At l,SCMPDS )),s +* (J +* (Start-At l,SCMPDS )) equal_outside NAT
let l be Element of NAT ; :: thesis: s +* (I +* (Start-At l,SCMPDS )),s +* (J +* (Start-At l,SCMPDS )) equal_outside NAT

A1: now

let a be Int_position ; :: thesis: (s +* (J +* (Start-At l,SCMPDS ))) . a = (s +* (I +* (Start-At l,SCMPDS ))) . a
A2: not a in dom (I +* (Start-At l,SCMPDS )) by SCMPDS_4:61;
not a in dom (J +* (Start-At l,SCMPDS )) by SCMPDS_4:61;
hence (s +* (J +* (Start-At l,SCMPDS ))) . a = s . a by FUNCT_4:12
.= (s +* (I +* (Start-At l,SCMPDS ))) . a by A2, FUNCT_4:12 ;
:: thesis: verum

end;

IC (s +* (J +* (Start-At l,SCMPDS ))) = IC ((s +* J) +* (Start-At l,SCMPDS )) by FUNCT_4:15
.= l by AMI_1:111
.= IC ((s +* I) +* (Start-At l,SCMPDS )) by AMI_1:111
.= IC (s +* (I +* (Start-At l,SCMPDS ))) by FUNCT_4:15 ;
hence s +* (I +* (Start-At l,SCMPDS )),s +* (J +* (Start-At l,SCMPDS )) equal_outside NAT by A1, SCMPDS_4:11; :: thesis: verum