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