let D be non empty set ; :: thesis: for m, n being Nat
for A being Matrix of n,m,D holds
( ( n = 0 implies m = 0 ) iff ( len A = n & width A = m ) )
let m, n 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_0:def 2;
hence ( len A = n & width A = m ) by A1, A2, MATRIX_0:def 3; :: thesis: verum

end;

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

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

end;

end;

end;

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