reconsider m1 = m, n1 = n as Element of NAT by ORDINAL1:def 12;
set a = the Element of D;
reconsider d = n1 |-> the Element of D 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 |-> the Element of D 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 |-> the Element of D)} by FUNCOP_1:13;
hence ( x = p & len p = n1 ) 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: ( len M = m & ( for p being FinSequence of D st p in rng M holds
len p = n ) )
thus len M = m by CARD_1:def 7; :: 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