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