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