let a be Int-Location ; :: thesis: for l being Element of NAT holds not a in dom (Start-At (l,SCM+FSA))
let l be Element of NAT ; :: thesis: not a in dom (Start-At (l,SCM+FSA))
A1: dom (Start-At (l,SCM+FSA)) = {(IC SCM+FSA)} by FUNCOP_1:19;
assume a in dom (Start-At (l,SCM+FSA)) ; :: thesis: contradiction
then a = IC SCM+FSA by A1, TARSKI:def 1;
hence contradiction by SCMFSA_2:81; :: thesis: verum