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 )

proof

reconsider p = n |-> the Element of D as FinSequence of D ;
take n ; :: thesis: for x being object st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n )
let x be object ; :: thesis: ( x in rng M implies ex p being FinSequence of D st
( x = p & len p = n ) )
assume A1: x in rng M ; :: thesis: ex p being FinSequence of D st
( x = p & len p = n )
take p ; :: thesis: ( x = p & len p = n )
rng M c= {(n |-> the Element of D)} by FUNCOP_1:13;
hence ( x = p & len p = n ) by A1, CARD_1:def 7, TARSKI:def 1; :: thesis: verum

end;

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