set A = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } ;
A1: X is finite ;
A2: { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } is finite from FRAENKEL:sch 21(A1);
for Y being set st Y in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } holds
Y is finite

proof

let Y be set ; :: thesis: ( Y in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } implies Y is finite )
assume Y in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } ; :: thesis: Y is finite
then ex i being Instruction of SCM+FSA st
( Y = UsedIntLoc i & i in X ) ;
hence Y is finite ; :: thesis: verum

end;

hence UsedILoc X is finite by A2, FINSET_1:7; :: thesis: verum