let D be non empty set ; :: thesis: for M being Matrix of D holds card (Values M) <= (len M) * (width M)
let M be Matrix of D; :: thesis: card (Values M) <= (len M) * (width M)
A1: card (dom (rngs M)) = card (dom M) by FUNCT_6:90
.= card (len M) by CARD_1:104 ;

now

let x be set ; :: thesis: ( x in dom (rngs M) implies card ((rngs M) . x) c= card (width M) )
assume x in dom (rngs M) ; :: thesis: card ((rngs M) . x) c= card (width M)
then A2: x in dom M by FUNCT_6:90;
then reconsider i = x as Element of NAT ;
reconsider f = M . i as FinSequence of D by Th1;
card (rng f) c= card (dom f) by CARD_2:80;
then card (rng f) c= card (Seg (len f)) by FINSEQ_1:def 3;
then card (rng f) c= card (len f) by FINSEQ_1:76;
then card (rng f) c= card (width M) by A2, Th4;
hence card ((rngs M) . x) c= card (width M) by A2, FUNCT_6:31; :: thesis: verum

end;

then card (Union (rngs M)) c= (card (len M)) *` (card (width M)) by A1, CARD_3:132;
then card (Values M) c= card ((len M) * (width M)) by CARD_2:52;
then card (Values M) <= card ((len M) * (width M)) by NAT_1:40;
hence card (Values M) <= (len M) * (width M) by CARD_1:def 5; :: thesis: verum