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: dom ((Initialized I) +* (I ';' J)) = (dom (Initialized I)) \/ (dom (I ';' J)) by FUNCT_4:def 1
.= (((dom I) \/ {(intloc 0 )}) \/ {(IC SCM+FSA )}) \/ (dom (I ';' J)) by Th43
.= ((dom I) \/ {(intloc 0 )}) \/ ({(IC SCM+FSA )} \/ (dom (I ';' J))) by XBOOLE_1:4
.= (dom I) \/ ({(intloc 0 )} \/ ((dom (I ';' J)) \/ {(IC SCM+FSA )})) by XBOOLE_1:4
.= (dom I) \/ (({(intloc 0 )} \/ (dom (I ';' J))) \/ {(IC SCM+FSA )}) by XBOOLE_1:4
.= ((dom I) \/ ((dom (I ';' J)) \/ {(intloc 0 )})) \/ {(IC SCM+FSA )} by XBOOLE_1:4
.= ((dom (I ';' J)) \/ {(intloc 0 )}) \/ {(IC SCM+FSA )} by A1, XBOOLE_1:4
.= dom (Initialized (I ';' J)) by Th43 ;

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 SCM+FSA ) by A3, Th44;

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

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

end;

suppose A7: 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 A7, Th46
.= (Initialized (I ';' J)) . x by A7, Th46 ;
:: thesis: verum

end;

suppose A8: x = IC SCM+FSA ; :: 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
.= insloc 0 by A8, Th46
.= (Initialized (I ';' J)) . x by A8, Th46 ;
:: thesis: verum

end;

end;

end;

hence (Initialized I) +* (I ';' J) = Initialized (I ';' J) by A2, FUNCT_1:9; :: thesis: verum