let n be Nat; :: thesis: for D being non empty set
for M being Matrix of D st len M = n holds
M is Matrix of n, width M,D
let D be non empty set ; :: thesis: for M being Matrix of D st len M = n holds
M is Matrix of n, width M,D
let M be Matrix of D; :: thesis: ( len M = n implies M is Matrix of n, width M,D )
assume that
A1: len M = n and
A2: M is not Matrix of n, width M,D ; :: thesis: contradiction
set m = width M;

per cases ( len M <> n or ex p being FinSequence of D st
( p in rng M & not len p = width M ) ) by A2, MATRIX_1:def 3;

suppose len M <> n ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose ex p being FinSequence of D st
( p in rng M & not len p = width M ) ; :: thesis: contradiction

then consider p being FinSequence of D such that
A3: p in rng M and
A4: len p <> width M ;
consider k being Nat such that
A5: for x being set st x in rng M holds
ex q being FinSequence of D st
( x = q & len q = k ) by MATRIX_1:9;
reconsider x = p as set ;
A6: ex q being FinSequence of D st
( x = q & len q = k ) by A3, A5;

now

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

suppose n = 0 ; :: thesis: len p = width M

then M = {} by A1;
hence len p = width M by A3, RELAT_1:60; :: thesis: verum

end;

suppose n > 0 ; :: thesis: len p = width M

then consider s being FinSequence such that
A7: s in rng M and
A8: len s = width M by A1, MATRIX_1:def 4;
reconsider y = s as set ;
ex r being FinSequence of D st
( y = r & len r = k ) by A5, A7;
hence len p = width M by A6, A8; :: thesis: verum

end;

end;

end;

hence contradiction by A4; :: thesis: verum

end;

end;