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

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

hence
UsedILoc X is finite
by A2, FINSET_1:7; :: thesis: verum
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;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