let I, J be Program of SCMPDS ; :: thesis: for s being State of SCMPDS st Initialized J c= s holds
s +* (Initialized I) = s +* I
let s be State of SCMPDS ; :: 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) \/ ((dom I) \/ {(IC SCMPDS )}) by Th27
.= ((dom J) \/ {(IC SCMPDS )}) \/ (dom I) by XBOOLE_1:4
.= (dom (Initialized J)) \/ (dom I) by Th27 ;
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 Th9;
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 = IC SCMPDS ) by A8, Th28;

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

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

end;

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

then A11: x in dom (Initialized J) by Th7;
A12: not x in dom I by A10, Th30;
thus (Initialized I) . x = 0 by A10, Th29
.= (Initialized J) . x by A10, Th29
.= s . x by A2, A11, GRFUNC_1:8
.= (s +* I) . x by A12, FUNCT_4:12 ; :: thesis: verum

end;

end;

end;

A13: 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 A14: 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, A14 ;
:: thesis: verum

end;

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

then A16: not x in dom I by A6;
thus (s +* (Initialized I)) . x = s . x by A15, FUNCT_4:12
.= (s +* I) . x by A16, 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 A13, FUNCT_1:9; :: thesis: verum