deffunc H₁( Function) -> set = rng D;
set A = { H₁(f) where f is Element of D * : f in rng M } ;

A1: now :: thesis: for X being set st X in { H₁(f) where f is Element of D * : f in rng M } holds
X is finite

let X be set ; :: thesis: ( X in { H₁(f) where f is Element of D * : f in rng M } implies X is finite )
assume X in { H₁(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 ;
{ H₁(f) where f is Element of D * : f in rng M } is finite from FRAENKEL:sch 21(A2);
then union { H₁(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