let I, J be Program of SCM+FSA; :: thesis: (Initialized I) +* (I ';' J) = Initialized (I ';' J)
A1: (dom I) \/ (dom (I ';' J)) = dom (I ';' J) by Th56, 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 = intloc 0 or x = IC ) by A3, Th44;

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

then x <> IC by COMPOS_1:139;
then not x in {(IC )} by TARSKI:def 1;
then A5: not x in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:19;
x <> intloc 0 by A4, Th47;
then not x in {(intloc 0)} by TARSKI:def 1;
then A6: not x in dom ((intloc 0) .--> 1) by FUNCOP_1:19;
A7: Initialized (I ';' J) = Initialize ((I ';' J) +* ((intloc 0) .--> 1)) by FUNCT_4:15;
thus ((Initialized I) +* (I ';' J)) . x = (I ';' J) . x by A4, FUNCT_4:14
.= ((I ';' J) +* ((intloc 0) .--> 1)) . x by A6, FUNCT_4:12
.= (Initialized (I ';' J)) . x by A5, FUNCT_4:12, A7 ; :: thesis: verum

end;

suppose A8: x = intloc 0 ; :: thesis: ((Initialized I) +* (I ';' J)) . b₁ = (Initialized (I ';' J)) . b₁

then not x in dom (I ';' J) by Th47;
hence ((Initialized I) +* (I ';' J)) . x = (Initialized I) . x by FUNCT_4:12
.= 1 by A8, Th46
.= (Initialized (I ';' J)) . x by A8, Th46 ;
:: thesis: verum

end;

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

then not x in dom (I ';' J) by COMPOS_1:139;
hence ((Initialized I) +* (I ';' J)) . x = (Initialized I) . x by FUNCT_4:12
.= 0 by A9, Th46
.= (Initialized (I ';' J)) . x by A9, Th46 ;
:: thesis: verum

end;

end;

end;

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