let w be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for I being Program of SCM+FSA holds dom ((Initialized I) +* (f .--> w)) = (dom I) \/ {(intloc 0 ),(IC SCM+FSA ),f}
let f be FinSeq-Location ; :: thesis: for I being Program of SCM+FSA holds dom ((Initialized I) +* (f .--> w)) = (dom I) \/ {(intloc 0 ),(IC SCM+FSA ),f}
let I be Program of SCM+FSA ; :: thesis: dom ((Initialized I) +* (f .--> w)) = (dom I) \/ {(intloc 0 ),(IC SCM+FSA ),f}
dom ((Initialized I) +* (f .--> w)) = (dom (Initialized I)) \/ (dom (f .--> w)) by FUNCT_4:def 1
.= (dom (Initialized I)) \/ {f} by FUNCOP_1:19
.= ((dom I) \/ {(intloc 0 ),(IC SCM+FSA )}) \/ {f} by Th41
.= (dom I) \/ ({(intloc 0 ),(IC SCM+FSA )} \/ {f}) by XBOOLE_1:4 ;
hence dom ((Initialized I) +* (f .--> w)) = (dom I) \/ {(intloc 0 ),(IC SCM+FSA ),f} by ENUMSET1:43; :: thesis: verum