let K be Field; :: thesis: for M being Matrix of K holds
( the_rank_of M = 0 iff M = 0. K,(len M),(width M) )
let M be Matrix of K; :: thesis: ( the_rank_of M = 0 iff M = 0. K,(len M),(width M) )
set NULL = 0. K,(len M),(width M);
reconsider M' = M as Matrix of len M, width M,K by MATRIX_2:7;
thus ( the_rank_of M = 0 implies M = 0. K,(len M),(width M) ) :: thesis: ( M = 0. K,(len M),(width M) implies the_rank_of M = 0 )

proof

assume A1: the_rank_of M = 0 ; :: thesis: M = 0. K,(len M),(width M)

now

let i, j be Nat; :: thesis: ( [i,j] in Indices M' implies M' * i,j = (0. K,(len M),(width M)) * i,j )
assume A2: [i,j] in Indices M' ; :: thesis: M' * i,j = (0. K,(len M),(width M)) * i,j
reconsider i' = i, j' = j as Element of NAT by ORDINAL1:def 13;
Indices M' = Indices (0. K,(len M),(width M)) by MATRIX_1:27;
then ( M * i',j' = 0. K & (0. K,(len M),(width M)) * i,j = 0. K ) by A1, A2, Th94, MATRIX_3:3;
hence M' * i,j = (0. K,(len M),(width M)) * i,j ; :: thesis: verum

end;

hence M = 0. K,(len M),(width M) by MATRIX_1:28; :: thesis: verum

end;

assume A3: M = 0. K,(len M),(width M) ; :: thesis: the_rank_of M = 0
assume the_rank_of M <> 0 ; :: thesis: contradiction
then the_rank_of M > 0 ;
then ex i, j being Nat st
( [i,j] in Indices M & M * i,j <> 0. K ) by Th94;
hence contradiction by A3, MATRIX_3:3; :: thesis: verum