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