let I be Program of SCM+FSA ; :: thesis: for f being FinSeq-Location
for l being Instruction-Location of SCM+FSA holds not f in dom (I +* (Start-At l))
let f be FinSeq-Location ; :: thesis: for l being Instruction-Location of SCM+FSA holds not f in dom (I +* (Start-At l))
let l be Instruction-Location of SCM+FSA ; :: thesis: not f in dom (I +* (Start-At l))
assume f in dom (I +* (Start-At l)) ; :: thesis: contradiction
then f in (dom I) \/ (dom (Start-At l)) by FUNCT_4:def 1;
then A1: ( f in dom I or f in dom (Start-At l) ) by XBOOLE_0:def 3;
A2: dom I c= NAT by RELAT_1:def 18;
f in FinSeq-Locations by SCMFSA_2:10;
hence contradiction by A1, A2, Th10, SCMFSA_2:14, XBOOLE_0:3; :: thesis: verum