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