set K = D;
set A = M;
A1: len M = n by Def2;
A2: for p being FinSequence of D st p in rng (M @) holds
len p = n

proof

let p be FinSequence of D; :: thesis: ( p in rng (M @) implies len p = n )
consider n2 being Nat such that
A3: for x being object st x in rng (M @) holds
ex s being FinSequence st
( s = x & len s = n2 ) by Def1;
A4: for p2 being FinSequence of D st p2 in rng (M @) holds
len p2 = n2

proof

let p2 be FinSequence of D; :: thesis: ( p2 in rng (M @) implies len p2 = n2 )
assume p2 in rng (M @) ; :: thesis: len p2 = n2
then ex s being FinSequence st
( s = p2 & len s = n2 ) by A3;
hence len p2 = n2 ; :: thesis: verum

end;

assume A5: p in rng (M @) ; :: thesis: len p = n
then A6: ex s being FinSequence st
( s = p & len s = n2 ) by A3;

per cases ( n > 0 or n <= 0 ) ;

suppose A7: n > 0 ; :: thesis: len p = n

then A8: width M = n by A1, Th20;
then A9: width (M @) = len M by A7, Th29;
A10: len (M @) = width M by A7, A8, Th29;
then M @ is Matrix of n,n2,D by A4, A8, Def2;
hence len p = n by A1, A6, A7, A8, A10, A9, Th20; :: thesis: verum

end;

suppose A11: n <= 0 ; :: thesis: len p = n

A12: ( len (M @) = width M & ex x0 being object st
( x0 in dom (M @) & p = (M @) . x0 ) ) by A5, Def6, FUNCT_1:def 3;
width M = 0 by A1, A11, Def3;
then Seg (width M) = {} ;
hence len p = n by A12, FINSEQ_1:def 3; :: thesis: verum

end;

end;

end;

A13: len (M @) = width M by Def6;

now :: thesis: len (M @) = n

per cases ( n > 0 or n = 0 ) ;

suppose n > 0 ; :: thesis: len (M @) = n

hence len (M @) = n by A13, A1, Th20; :: thesis: verum

end;

suppose n = 0 ; :: thesis: len (M @) = n

hence len (M @) = n by A13, A1, Def3; :: thesis: verum

end;

end;

end;

hence M @ is n,n -size by A2; :: thesis: verum