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