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