let l be Element of NAT ; :: thesis: not l in dom (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))
assume l in dom (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) ; :: thesis: contradiction
then ( l = intloc 0 or l = IC SCM+FSA ) by Th1;
hence contradiction by AMI_1:48, SCMFSA_2:84; :: thesis: verum