let D be non empty set ; :: thesis: for n, m being Nat
for A being Matrix of n,m,D holds
( ( n = 0 implies m = 0 ) iff ( len A = n & width A = m ) )
let n, m be Nat; :: thesis: for A being Matrix of n,m,D holds
( ( n = 0 implies m = 0 ) iff ( len A = n & width A = m ) )
let A be Matrix of n,m,D; :: thesis: ( ( n = 0 implies m = 0 ) iff ( len A = n & width A = m ) )
thus ( ( n = 0 implies m = 0 ) implies ( len A = n & width A = m ) ) :: thesis: ( len A = n & width A = m & n = 0 implies m = 0 )

proof

assume A1: ( n = 0 implies m = 0 ) ; :: thesis: ( len A = n & width A = m )

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

suppose A2: n = 0 ; :: thesis: ( len A = n & width A = m )

then len A = 0 by MATRIX_1:def 3;
hence ( len A = n & width A = m ) by A1, A2, MATRIX_1:def 4; :: thesis: verum

end;

suppose A3: n > 0 ; :: thesis: ( len A = n & width A = m )

len A = n by MATRIX_1:def 3;
hence ( len A = n & width A = m ) by A3, MATRIX_1:20; :: thesis: verum

end;

end;

end;

thus ( len A = n & width A = m & n = 0 implies m = 0 ) by MATRIX_1:def 4; :: thesis: verum