let I, J be Program of SCMPDS ; :: thesis: (Initialized I) +* (I ';' J) = Initialized (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 (Initialized (I ';' J)) implies ((Initialized I) +* (I ';' J)) . b₁ = (Initialized (I ';' J)) . b₁ )
assume A3: x in dom (Initialized (I ';' J)) ; :: thesis: ((Initialized I) +* (I ';' J)) . b₁ = (Initialized (I ';' J)) . b₁

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

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

then x <> IC SCMPDS by Th30;
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 ((Initialized I) +* (I ';' J)) . x = (I ';' J) . x by A4, FUNCT_4:14
.= (Initialized (I ';' J)) . x by A5, FUNCT_4:12 ; :: thesis: verum

end;

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

then not x in dom (I ';' J) by Th30;
hence ((Initialized I) +* (I ';' J)) . x = (Initialized I) . x by FUNCT_4:12
.= 0 by A6, Th29
.= (Initialized (I ';' J)) . x by A6, Th29 ;
:: thesis: verum

end;

end;

end;

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