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, Def2;

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

hence contradiction by A1; :: thesis: verum

end;

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

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

now :: thesis: len p = width M

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 A5; :: thesis: verum

end;

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

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

end;

end;

end;

hence contradiction by A6; :: thesis: verum

end;

end;