let I, J be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st Initialized J c= s holds
s +* (Initialized I) = s +* I
let s be State of SCM+FSA ; :: thesis: ( Initialized J c= s implies s +* (Initialized I) = s +* I )
set s1 = s +* I;
assume A1: Initialized J c= s ; :: thesis: s +* (Initialized I) = s +* I
then A2: dom (Initialized J) c= dom s by GRFUNC_1:8;
(dom J) \/ (dom (Initialized I)) = (dom J) \/ (({(intloc 0 )} \/ (dom I)) \/ {(IC SCM+FSA )}) by Th43
.= (dom J) \/ (({(intloc 0 )} \/ {(IC SCM+FSA )}) \/ (dom I)) by XBOOLE_1:4
.= ((dom J) \/ ({(intloc 0 )} \/ {(IC SCM+FSA )})) \/ (dom I) by XBOOLE_1:4
.= (((dom J) \/ {(intloc 0 )}) \/ {(IC SCM+FSA )}) \/ (dom I) by XBOOLE_1:4
.= (dom (Initialized J)) \/ (dom I) by Th43 ;
then (dom J) \/ (dom (Initialized I)) c= (dom s) \/ (dom I) by A2, XBOOLE_1:13;
then (dom J) \/ (dom (Initialized I)) c= dom (s +* I) by FUNCT_4:def 1;
then A3: dom (Initialized I) c= dom (s +* I) by XBOOLE_1:11;

A4: now

let x be set ; :: thesis: ( x in dom (Initialized I) implies (Initialized I) . b₁ = (s +* I) . b₁ )
assume A5: x in dom (Initialized I) ; :: thesis: (Initialized I) . b₁ = (s +* I) . b₁

per cases ( x in dom I or x = intloc 0 or x = IC SCM+FSA ) by A5, Th44;

suppose A6: x in dom I ; :: thesis: (Initialized I) . b₁ = (s +* I) . b₁

hence (Initialized I) . x = I . x by Th50
.= (s +* I) . x by A6, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A7: x = intloc 0 ; :: thesis: (Initialized I) . b₁ = (s +* I) . b₁

then A8: not x in dom I by Th47;
A9: x in dom (Initialized J) by A7, Th45;
thus (Initialized I) . x = 1 by A7, Th46
.= (Initialized J) . x by A7, Th46
.= s . x by A1, A9, GRFUNC_1:8
.= (s +* I) . x by A8, FUNCT_4:12 ; :: thesis: verum

end;

suppose A10: x = IC SCM+FSA ; :: thesis: (Initialized I) . b₁ = (s +* I) . b₁

then A11: not x in dom I by Th47;
A12: x in dom (Initialized J) by A10, Th24;
thus (Initialized I) . x = insloc 0 by A10, Th46
.= (Initialized J) . x by A10, Th46
.= s . x by A1, A12, GRFUNC_1:8
.= (s +* I) . x by A11, FUNCT_4:12 ; :: thesis: verum

end;

end;

end;

A13: dom (s +* I) = (dom s) \/ (dom I) by FUNCT_4:def 1;
A14: dom (s +* (Initialized I)) = (dom s) \/ (dom (Initialized I)) by FUNCT_4:def 1;
I c= Initialized I by Th26;
then A15: dom I c= dom (Initialized I) by GRFUNC_1:8;
then A16: dom (s +* I) c= dom (s +* (Initialized I)) by A13, A14, XBOOLE_1:9;
dom (s +* (Initialized I)) c= (dom s) \/ ((dom s) \/ (dom I)) by A3, A13, A14, XBOOLE_1:9;
then dom (s +* (Initialized I)) c= ((dom s) \/ (dom s)) \/ (dom I) by XBOOLE_1:4;
then A17: dom (s +* (Initialized I)) = dom (s +* I) by A13, A16, XBOOLE_0:def 10;

now

let x be set ; :: thesis: ( x in dom (s +* (Initialized I)) implies (s +* (Initialized I)) . b₁ = (s +* I) . b₁ )
assume x in dom (s +* (Initialized I)) ; :: thesis: (s +* (Initialized I)) . b₁ = (s +* I) . b₁

per cases ( x in dom (Initialized I) or not x in dom (Initialized I) ) ;

suppose A18: x in dom (Initialized I) ; :: thesis: (s +* (Initialized I)) . b₁ = (s +* I) . b₁

hence (s +* (Initialized I)) . x = (Initialized I) . x by FUNCT_4:14
.= (s +* I) . x by A4, A18 ;
:: thesis: verum

end;

suppose A19: not x in dom (Initialized I) ; :: thesis: (s +* (Initialized I)) . b₁ = (s +* I) . b₁

then A20: not x in dom I by A15;
thus (s +* (Initialized I)) . x = s . x by A19, FUNCT_4:12
.= (s +* I) . x by A20, FUNCT_4:12 ; :: thesis: verum

end;

end;

end;

hence s +* (Initialized I) = s +* I by A17, FUNCT_1:9; :: thesis: verum