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;
A1: dom (s +* I) = (dom s) \/ (dom I) by FUNCT_4:def 1;
assume A2: Initialized J c= s ; :: thesis: s +* (Initialized I) = s +* I
then A3: dom (Initialized J) c= dom s by GRFUNC_1:8;
A4: dom (s +* (Initialized I)) = (dom s) \/ (dom (Initialized I)) by FUNCT_4:def 1;
(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 A3, XBOOLE_1:13;
then (dom J) \/ (dom (Initialized I)) c= dom (s +* I) by FUNCT_4:def 1;
then dom (Initialized I) c= dom (s +* I) by XBOOLE_1:11;
then dom (s +* (Initialized I)) c= (dom s) \/ ((dom s) \/ (dom I)) by A1, A4, XBOOLE_1:9;
then A5: dom (s +* (Initialized I)) c= ((dom s) \/ (dom s)) \/ (dom I) by XBOOLE_1:4;
I c= Initialized I by Th26;
then A6: dom I c= dom (Initialized I) by GRFUNC_1:8;

A7: now

let x be set ; :: thesis: ( x in dom (Initialized I) implies (Initialized I) . b₁ = (s +* I) . b₁ )
assume A8: 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 A8, Th44;

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

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

end;

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

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

end;

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

then A14: x in dom (Initialized J) by Th24;
A15: not x in dom I by A13, COMPOS_1:139;
thus (Initialized I) . x = 0 by A13, Th46
.= (Initialized J) . x by A13, Th46
.= s . x by A2, A14, GRFUNC_1:8
.= (s +* I) . x by A15, FUNCT_4:12 ; :: thesis: verum

end;

end;

end;

A16: 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 A17: 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 A7, A17 ;
:: thesis: verum

end;

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

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

end;

end;

end;

dom (s +* I) c= dom (s +* (Initialized I)) by A1, A4, A6, XBOOLE_1:9;
then dom (s +* (Initialized I)) = dom (s +* I) by A1, A5, XBOOLE_0:def 10;
hence s +* (Initialized I) = s +* I by A16, FUNCT_1:9; :: thesis: verum