let p be Program of ; :: thesis: for s being State of SCM+FSA holds (UsedI*Loc p) \/ (UsedILoc p) c= dom s
let s be State of SCM+FSA; :: thesis: (UsedI*Loc p) \/ (UsedILoc p) c= dom s
Int-Locations c= dom s by SCMFSA_2:45;
then A1: UsedILoc p c= dom s by XBOOLE_1:1;
FinSeq-Locations c= dom s by SCMFSA_2:46;
then UsedI*Loc p c= dom s by XBOOLE_1:1;
hence (UsedI*Loc p) \/ (UsedILoc p) c= dom s by A1, XBOOLE_1:8; :: thesis: verum