thus dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def 1
.= (dom ((intloc 0) .--> 1)) \/ {(IC )}
.= {(intloc 0)} \/ {(IC )}
.= {(intloc 0),(IC )} by ENUMSET1:1 ; :: thesis: verum