let w be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for I being Program of {INT,(INT *)} holds dom ((Initialized I) +* (f .--> w)) = (dom I) \/ {(intloc 0),(IC ),f}
let f be FinSeq-Location ; :: thesis: for I being Program of {INT,(INT *)} holds dom ((Initialized I) +* (f .--> w)) = (dom I) \/ {(intloc 0),(IC ),f}
let I be Program of {INT,(INT *)}; :: thesis: dom ((Initialized I) +* (f .--> w)) = (dom I) \/ {(intloc 0),(IC ),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 )}) \/ {f} by Th41
.= (dom I) \/ ({(intloc 0),(IC )} \/ {f}) by XBOOLE_1:4 ;
hence dom ((Initialized I) +* (f .--> w)) = (dom I) \/ {(intloc 0),(IC ),f} by ENUMSET1:43; :: thesis: verum