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: now :: thesis: for x being object st x in dom (rngs M) holds
card ((rngs M) . x) c= card (width M)

let x be object ; :: 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:60;
then reconsider i = x as Element of NAT ;
reconsider f = M . i as FinSequence of D by Th34;
card (rng f) c= card (dom f) by CARD_2:61;
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:55;
then card (rng f) c= card (width M) by A2, Th36;
hence card ((rngs M) . x) c= card (width M) by A2, FUNCT_6:22; :: thesis: verum

end;

card (dom (rngs M)) = card (dom M) by FUNCT_6:60
.= card (len M) by CARD_1:62 ;
then card (Union (rngs M)) c= (card (len M)) *` (card (width M)) by A1, CARD_2:86;
then Segm (card (Values M)) c= Segm (card ((len M) * (width M))) by CARD_2:39;
then card (Values M) <= card ((len M) * (width M)) by NAT_1:39;
hence card (Values M) <= (len M) * (width M) ; :: thesis: verum