let D be non empty set ; :: thesis: for M being Matrix of D st len M > 0 holds
for n being Nat holds
( M is Matrix of len M,n,D iff n = width M )
let M be Matrix of D; :: thesis: ( len M > 0 implies for n being Nat holds
( M is Matrix of len M,n,D iff n = width M ) )
assume A1: len M > 0 ; :: thesis: for n being Nat holds
( M is Matrix of len M,n,D iff n = width M )
let n be Nat; :: thesis: ( M is Matrix of len M,n,D iff n = width M )
thus ( M is Matrix of len M,n,D implies n = width M ) :: thesis: ( n = width M implies M is Matrix of len M,n,D )

proof

consider s being FinSequence such that
A2: s in rng M and
A3: len s = width M by A1, Def3;
rng M c= D * by FINSEQ_1:def 4;
then reconsider q = s as FinSequence of D by A2, FINSEQ_1:def 11;
assume M is Matrix of len M,n,D ; :: thesis: n = width M
then len q = n by A2, Def2;
hence n = width M by A3; :: thesis: verum

end;

assume n = width M ; :: thesis: M is Matrix of len M,n,D
then for p being FinSequence of D st p in rng M holds
len p = n by A1, Def3;
hence M is Matrix of len M,n,D by Def2; :: thesis: verum