let K be Field; :: thesis: for M1 being Matrix of K st len M1 > 0 holds

(0. K) * M1 = 0. (K,(len M1),(width M1))

let M1 be Matrix of K; :: thesis: ( len M1 > 0 implies (0. K) * M1 = 0. (K,(len M1),(width M1)) )

A1: len (0. (K,(len M1),(width M1))) = len M1 by MATRIX_0:def 2;

assume len M1 > 0 ; :: thesis: (0. K) * M1 = 0. (K,(len M1),(width M1))

then A2: width (0. (K,(len M1),(width M1))) = width M1 by A1, MATRIX_0:20;

A3: for i, j being Nat st [i,j] in Indices (0. (K,(len M1),(width M1))) holds

((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j)

hence (0. K) * M1 = 0. (K,(len M1),(width M1)) by A1, A2, A3, MATRIX_0:21; :: thesis: verum

(0. K) * M1 = 0. (K,(len M1),(width M1))

let M1 be Matrix of K; :: thesis: ( len M1 > 0 implies (0. K) * M1 = 0. (K,(len M1),(width M1)) )

A1: len (0. (K,(len M1),(width M1))) = len M1 by MATRIX_0:def 2;

assume len M1 > 0 ; :: thesis: (0. K) * M1 = 0. (K,(len M1),(width M1))

then A2: width (0. (K,(len M1),(width M1))) = width M1 by A1, MATRIX_0:20;

A3: for i, j being Nat st [i,j] in Indices (0. (K,(len M1),(width M1))) holds

((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j)

proof

( len ((0. K) * M1) = len M1 & width ((0. K) * M1) = width M1 )
by MATRIX_3:def 5;
let i, j be Nat; :: thesis: ( [i,j] in Indices (0. (K,(len M1),(width M1))) implies ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j) )

assume A4: [i,j] in Indices (0. (K,(len M1),(width M1))) ; :: thesis: ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j)

Indices (0. (K,(len M1),(width M1))) = Indices M1 by A1, A2, MATRIX_4:55;

then A5: ((0. K) * M1) * (i,j) = (0. K) * (M1 * (i,j)) by A4, MATRIX_3:def 5;

(0. (K,(len M1),(width M1))) * (i,j) = 0. K by A4, MATRIX_3:1;

hence ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j) by A5; :: thesis: verum

end;assume A4: [i,j] in Indices (0. (K,(len M1),(width M1))) ; :: thesis: ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j)

Indices (0. (K,(len M1),(width M1))) = Indices M1 by A1, A2, MATRIX_4:55;

then A5: ((0. K) * M1) * (i,j) = (0. K) * (M1 * (i,j)) by A4, MATRIX_3:def 5;

(0. (K,(len M1),(width M1))) * (i,j) = 0. K by A4, MATRIX_3:1;

hence ((0. K) * M1) * (i,j) = (0. (K,(len M1),(width M1))) * (i,j) by A5; :: thesis: verum

hence (0. K) * M1 = 0. (K,(len M1),(width M1)) by A1, A2, A3, MATRIX_0:21; :: thesis: verum