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

A1: now

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

end;

A3: now

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

end;

IC (s +* (I2 +* (Start-At l,SCM+FSA ))) = IC ((s +* I2) +* (Start-At l,SCM+FSA )) by FUNCT_4:15
.= l by FUNCT_4:121
.= IC ((s +* I1) +* (Start-At l,SCM+FSA )) by FUNCT_4:121
.= IC (s +* (I1 +* (Start-At l,SCM+FSA ))) by FUNCT_4:15 ;
hence s +* (I1 +* (Start-At l,SCM+FSA )),s +* (I2 +* (Start-At l,SCM+FSA )) equal_outside NAT by A1, A3, SCMFSA10:91; :: thesis: verum