set A = { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } ;
union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } c= FinSeq-Locations

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } or e in FinSeq-Locations )
assume e in union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } ; :: thesis: e in FinSeq-Locations
then consider B being set such that
A1: e in B and
A2: B in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } by TARSKI:def 4;
ex i being Instruction of SCM+FSA st
( B = UsedInt*Loc i & i in X ) by A2;
then B c= FinSeq-Locations by FINSUB_1:def 5;
hence e in FinSeq-Locations by A1; :: thesis: verum

end;

hence union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } is Subset of FinSeq-Locations ; :: thesis: verum