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 M9 = 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

A2: Indices M9 = Indices (0. K,(len M),(width M)) by MATRIX_1:27;
let i, j be Nat; :: thesis: ( [i,j] in Indices M9 implies M9 * i,j = (0. K,(len M),(width M)) * i,j )
assume A3: [i,j] in Indices M9 ; :: thesis: M9 * i,j = (0. K,(len M),(width M)) * i,j
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 13;
M * i9,j9 = 0. K by A1, A3, Th94;
hence M9 * 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