set A = { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } ;
A1: X is finite ;
A2: { (UsedInt*Loc 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 { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } holds
Y is finite
proof
let Y be set ; :: thesis: ( Y in { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } implies Y is finite )
assume Y in { (UsedInt*Loc 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 = UsedInt*Loc i & i in X ) ;
hence Y is finite ; :: thesis: verum
end;
hence UsedI*Loc X is finite by A2, FINSET_1:7; :: thesis: verum