thus dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) = (dom ((intloc 0 ) .--> 1)) \/ (dom (Start-At (insloc 0 ))) 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 ; :: thesis: verum