let I, J be Program of SCMPDS ; :: thesis: for s being State of SCMPDS st Initialize J c= s holds
(Initialize s) +* I = s +* I
let s be State of SCMPDS ; :: thesis: ( Initialize J c= s implies (Initialize s) +* I = s +* I )
set s1 = s +* I;
A1: dom (s +* I) = (dom s) \/ (dom I) by FUNCT_4:def 1;
I1: (Initialize s) +* I = s +* (Initialize I) by Th5;
assume A2: Initialize J c= s ; :: thesis: (Initialize s) +* I = s +* I
then A3: dom (Initialize J) c= dom s by GRFUNC_1:8;
A4: dom ((Initialize s) +* I) = (dom s) \/ (dom (Initialize I)) by I1, FUNCT_4:def 1;
(dom J) \/ (dom (Initialize I)) = (dom J) \/ ((dom I) \/ {(IC SCMPDS )}) by COMPOS_1:76
.= ((dom J) \/ {(IC SCMPDS )}) \/ (dom I) by XBOOLE_1:4
.= (dom (Initialize J)) \/ (dom I) by COMPOS_1:76 ;
then (dom J) \/ (dom (Initialize I)) c= (dom s) \/ (dom I) by A3, XBOOLE_1:13;
then (dom J) \/ (dom (Initialize I)) c= dom (s +* I) by FUNCT_4:def 1;
then dom (Initialize I) c= dom (s +* I) by XBOOLE_1:11;
then dom ((Initialize s) +* I) c= (dom s) \/ ((dom s) \/ (dom I)) by A1, A4, XBOOLE_1:9;
then A5: dom ((Initialize s) +* I) c= ((dom s) \/ (dom s)) \/ (dom I) by XBOOLE_1:4;
I c= Initialize I by Th9;
then A6: dom I c= dom (Initialize I) by GRFUNC_1:8;

A7: now

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

per cases ( x in dom I or x = IC SCMPDS ) by A8, COMPOS_1:77;

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

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

end;

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

then A11: x in dom (Initialize J) by COMPOS_1:def 16;
A12: not x in dom I by A10, COMPOS_1:3;
thus (Initialize I) . x = IC (Initialize I) by A10
.= 0 by COMPOS_1:def 16
.= IC (Initialize J) by COMPOS_1:def 16
.= s . x by A2, A10, A11, GRFUNC_1:8
.= (s +* I) . x by A12, FUNCT_4:12 ; :: thesis: verum

end;

end;

end;

I1: (Initialize s) +* I = s +* (Initialize I) by Th5;

A13: now

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

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

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

hence ((Initialize s) +* I) . x = (Initialize I) . x by I1, FUNCT_4:14
.= (s +* I) . x by A7, A14 ;
:: thesis: verum

end;

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

then A16: not x in dom I by A6;
thus ((Initialize s) +* I) . x = s . x by A15, I1, FUNCT_4:12
.= (s +* I) . x by A16, FUNCT_4:12 ; :: thesis: verum

end;

end;

end;

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