reconsider m1 = m, n1 = n as Element of NAT by ORDINAL1:def 13;
consider a being Element of D;
reconsider d = n1 |-> a as Element of D * by FINSEQ_1:def 11;
reconsider M = m1 |-> d as FinSequence of D * ;
ex n being Element of NAT st
for x being set st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n )

proof

reconsider p = n1 |-> a as FinSequence of D ;
take n1 ; :: thesis: for x being set st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n1 )
let x be set ; :: thesis: ( x in rng M implies ex p being FinSequence of D st
( x = p & len p = n1 ) )
assume A1: x in rng M ; :: thesis: ex p being FinSequence of D st
( x = p & len p = n1 )
take p ; :: thesis: ( x = p & len p = n1 )
rng M c= {(n |-> a)} by FUNCOP_1:19;
hence ( x = p & len p = n1 ) by A1, FINSEQ_1:def 18, TARSKI:def 1; :: thesis: verum

end;

then reconsider M = M as Matrix of D by Th9;
take M ; :: thesis: ( len M = m & ( for p being FinSequence of D st p in rng M holds
len p = n ) )
thus len M = m by FINSEQ_1:def 18; :: 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 |-> a)} by FUNCOP_1:19;
assume p in rng M ; :: thesis: len p = n
then p = n |-> a by A2, TARSKI:def 1;
hence len p = n by FINSEQ_1:def 18; :: thesis: verum