let s be State of ; :: thesis: for I1, I2 being Program of
for l being Instruction-Location of SCM+FSA holds s +* (I1 +* (Start-At l)),s +* (I2 +* (Start-At l)) equal_outside NAT
let I1, I2 be Program of ; :: thesis: for l being Instruction-Location of SCM+FSA holds s +* (I1 +* (Start-At l)),s +* (I2 +* (Start-At l)) equal_outside NAT
let l be Instruction-Location of SCM+FSA ; :: thesis: s +* (I1 +* (Start-At l)),s +* (I2 +* (Start-At l)) equal_outside NAT

A1: now

let a be Int-Location ; :: thesis: (s +* (I2 +* (Start-At l))) . a = (s +* (I1 +* (Start-At l))) . a
A2: not a in dom (I1 +* (Start-At l)) by SCMFSA6B:12;
not a in dom (I2 +* (Start-At l)) by SCMFSA6B:12;
hence (s +* (I2 +* (Start-At l))) . a = s . a by FUNCT_4:12
.= (s +* (I1 +* (Start-At l))) . a by A2, FUNCT_4:12 ;
:: thesis: verum

end;

A3: now

let f be FinSeq-Location ; :: thesis: (s +* (I2 +* (Start-At l))) . f = (s +* (I1 +* (Start-At l))) . f
A4: not f in dom (I1 +* (Start-At l)) by SCMFSA6B:13;
not f in dom (I2 +* (Start-At l)) by SCMFSA6B:13;
hence (s +* (I2 +* (Start-At l))) . f = s . f by FUNCT_4:12
.= (s +* (I1 +* (Start-At l))) . f by A4, FUNCT_4:12 ;
:: thesis: verum

end;

IC (s +* (I2 +* (Start-At l))) = IC ((s +* I2) +* (Start-At l)) by FUNCT_4:15
.= l by AMI_1:111
.= IC ((s +* I1) +* (Start-At l)) by AMI_1:111
.= IC (s +* (I1 +* (Start-At l))) by FUNCT_4:15 ;
hence s +* (I1 +* (Start-At l)),s +* (I2 +* (Start-At l)) equal_outside NAT by A1, A3, SCMFSA6A:28; :: thesis: verum