let I, J be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA holds s +* (Initialized I),s +* (Initialized J) equal_outside NAT
let s be State of SCM+FSA ; :: thesis: s +* (Initialized I),s +* (Initialized J) equal_outside NAT
A1: ( intloc 0 in dom (Initialized I) & IC SCM+FSA in dom (Initialized I) & intloc 0 in dom (Initialized J) & IC SCM+FSA in dom (Initialized J) ) by Th24, Th45;
then A2: IC (s +* (Initialized J)) = (Initialized J) . (IC SCM+FSA ) by FUNCT_4:14
.= insloc 0 by Th46
.= (Initialized I) . (IC SCM+FSA ) by Th46
.= IC (s +* (Initialized I)) by A1, FUNCT_4:14 ;

A3: now

let a be Int-Location ; :: thesis: (s +* (Initialized J)) . b₁ = (s +* (Initialized I)) . b₁

per cases ( a = intloc 0 or a <> intloc 0 ) ;

suppose A4: a = intloc 0 ; :: thesis: (s +* (Initialized J)) . b₁ = (s +* (Initialized I)) . b₁

hence (s +* (Initialized J)) . a = (Initialized J) . a by A1, FUNCT_4:14
.= 1 by A4, Th46
.= (Initialized I) . a by A4, Th46
.= (s +* (Initialized I)) . a by A1, A4, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A5: a <> intloc 0 ; :: thesis: (s +* (Initialized J)) . b₁ = (s +* (Initialized I)) . b₁

then A6: not a in dom (Initialized I) by Th48;
not a in dom (Initialized J) by A5, Th48;
hence (s +* (Initialized J)) . a = s . a by FUNCT_4:12
.= (s +* (Initialized I)) . a by A6, FUNCT_4:12 ;
:: thesis: verum

end;

end;

end;

now

let f be FinSeq-Location ; :: thesis: (s +* (Initialized J)) . f = (s +* (Initialized I)) . f
A7: not f in dom (Initialized I) by Th49;
not f in dom (Initialized J) by Th49;
hence (s +* (Initialized J)) . f = s . f by FUNCT_4:12
.= (s +* (Initialized I)) . f by A7, FUNCT_4:12 ;
:: thesis: verum

end;

hence s +* (Initialized I),s +* (Initialized J) equal_outside NAT by A2, A3, Th28; :: thesis: verum