let w be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for I being Program of holds dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f}
let f be FinSeq-Location ; :: thesis: for I being Program of holds dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f}
let I be Program of ; :: thesis: dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f}
Initialized (f .--> w) = (f .--> w) +* (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:def 3;
then dom (Initialized (f .--> w)) = (dom (Initialize ((intloc 0) .--> 1))) \/ (dom (f .--> w)) by FUNCT_4:def 1
.= (dom (Initialize ((intloc 0) .--> 1))) \/ {f} by FUNCOP_1:13
.= {(intloc 0),(IC )} \/ {f} by SCMFSA6A:42
.= {(intloc 0),(IC )} \/ {f} ;
hence dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f} by ENUMSET1:3; :: thesis: verum