let l be Nat; :: thesis: for f being FinSeq-Location holds not f in dom (Start-At (l,SCM+FSA))
let f be FinSeq-Location ; :: thesis: not f in dom (Start-At (l,SCM+FSA))
assume f in dom (Start-At (l,SCM+FSA)) ; :: thesis: contradiction
then f = IC by TARSKI:def 1;
hence contradiction by Th50; :: thesis: verum