deffunc H1( Function) -> set = rng D;
set A = { H1(f) where f is Element of D * : f in rng M } ;
A1: now :: thesis: for X being set st X in { H1(f) where f is Element of D * : f in rng M } holds
X is finite
let X be set ; :: thesis: ( X in { H1(f) where f is Element of D * : f in rng M } implies X is finite )
assume X in { H1(f) where f is Element of D * : f in rng M } ; :: thesis: X is finite
then ex f being Element of D * st
( X = rng f & f in rng M ) ;
hence X is finite ; :: thesis: verum
end;
A2: rng M is finite ;
{ H1(f) where f is Element of D * : f in rng M } is finite from FRAENKEL:sch 21(A2);
 then union { H1(f) where f is Element of D * : f in rng M } is finite by A1, FINSET_1:7;
hence Values M is finite by Th35; :: thesis: verum