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