set a = the Element of D;
reconsider d = n |-> the Element of D as Element of D * by FINSEQ_1:def 11;
reconsider M = m |-> d as FinSequence of D * ;
ex n being Nat st
for x being object st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n ) then reconsider M = M as Matrix of D by Th9;
take M ; :: thesis: M is m,n -size
thus len M = m by CARD_1:def 7; :: according to MATRIX_0:def 2 :: thesis: for p being FinSequence of D st p in rng M holds
len p = n
let p be FinSequence of D; :: thesis: ( p in rng M implies len p = n )
A2: rng M c= {(n |-> the Element of D)} by FUNCOP_1:13;
assume p in rng M ; :: thesis: len p = n
then p = n |-> the Element of D by A2, TARSKI:def 1;
hence len p = n by CARD_1:def 7; :: thesis: verum