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_0:51;
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 :: thesis: for i, j being Nat st [i,j] in Indices M9 holds
M9 * (i,j) = (0. (K,(len M),(width M))) * (i,j)

A2: Indices M9 = Indices (0. (K,(len M),(width M))) by MATRIX_0:26;
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 12;
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:1; :: thesis: verum

end;

hence M = 0. (K,(len M),(width M)) by MATRIX_0:27; :: 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:1; :: thesis: verum