let I, J be Program of SCMPDS ; :: thesis: (Initialize I) +* (I ';' J) = Initialize (I ';' J)
A1: (dom I) \/ (dom (I ';' J)) = dom (I ';' J) by Th39, XBOOLE_1:12;

A2: now

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

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

suppose A4: x in dom (I ';' J) ; :: thesis: ((Initialize I) +* (I ';' J)) . b₁ = (Initialize (I ';' J)) . b₁

then x <> IC SCMPDS by COMPOS_1:3;
then not x in {(IC SCMPDS )} by TARSKI:def 1;
then A5: not x in dom (Start-At 0 ,SCMPDS ) by FUNCOP_1:19;
thus ((Initialize I) +* (I ';' J)) . x = (I ';' J) . x by A4, FUNCT_4:14
.= (Initialize (I ';' J)) . x by A5, FUNCT_4:12 ; :: thesis: verum

end;

suppose A6: x = IC SCMPDS ; :: thesis: ((Initialize I) +* (I ';' J)) . b₁ = (Initialize (I ';' J)) . b₁

then not x in dom (I ';' J) by COMPOS_1:3;
hence ((Initialize I) +* (I ';' J)) . x = IC (Initialize I) by A6, FUNCT_4:12
.= 0 by COMPOS_1:def 16
.= IC (Initialize (I ';' J)) by COMPOS_1:def 16
.= (Initialize (I ';' J)) . x by A6 ;
:: thesis: verum

end;

end;

end;

dom ((Initialize I) +* (I ';' J)) = (dom (Initialize I)) \/ (dom (I ';' J)) by FUNCT_4:def 1
.= ((dom I) \/ {(IC SCMPDS )}) \/ (dom (I ';' J)) by COMPOS_1:76
.= ((dom I) \/ (dom (I ';' J))) \/ {(IC SCMPDS )} by XBOOLE_1:4
.= dom (Initialize (I ';' J)) by A1, COMPOS_1:76 ;
hence (Initialize I) +* (I ';' J) = Initialize (I ';' J) by A2, FUNCT_1:9; :: thesis: verum