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 FUNCT_4:121
.= IC ((s +* I) +* (Start-At (l,SCMPDS))) by FUNCT_4:121
.= 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