set A = { (rng f) where f is Element of D * : f in rng M } ;
for X being set st X in { (rng f) where f is Element of D * : f in rng M } holds
X c= D
proof
let X be set ; :: thesis: ( X in { (rng f) where f is Element of D * : f in rng M } implies X c= D )
assume X in { (rng f) where f is Element of D * : f in rng M } ; :: thesis: X c= D
then ex f being Element of D * st
( X = rng f & f in rng M ) ;
hence X c= D ; :: thesis: verum
end;
then union { (rng f) where f is Element of D * : f in rng M } c= D by ZFMISC_1:76;
hence Values M is Subset of D by MATRIX_0:35; :: thesis: verum