let K be Field; :: thesis: for M being Matrix of holds
( the_rank_of M = 0 iff M = 0. K,(len M),(width M) )
let M be Matrix of ; :: 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 the carrier of K, len M, 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

A2: Indices M' = Indices (0. K,(len M),(width M)) by MATRIX_1:27;
let i, j be Nat; :: thesis: ( [i,j] in Indices M' implies M' * i,j = (0. K,(len M),(width M)) * i,j )
assume A3: [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;
M * i',j' = 0. K by A1, A3, Th94;
hence M' * i,j = (0. K,(len M),(width M)) * i,j by A3, A2, MATRIX_3:3; :: thesis: verum

end;

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

end;

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