let n, m be Nat; :: thesis: for K being Field
for i, j being Nat st [i,j] in Indices (0. K,n,m) holds
(0. K,n,m) * i,j = 0. K
let K be Field; :: thesis: for i, j being Nat st [i,j] in Indices (0. K,n,m) holds
(0. K,n,m) * i,j = 0. K
let i, j be Nat; :: thesis: ( [i,j] in Indices (0. K,n,m) implies (0. K,n,m) * i,j = 0. K )
assume A1: [i,j] in Indices (0. K,n,m) ; :: thesis: (0. K,n,m) * i,j = 0. K
A2: Indices (0. K,n,m) = [:(Seg n),(Seg (width (0. K,n,m))):] by MATRIX_1:26;

per cases ( n > 0 or n = 0 ) ;

suppose n > 0 ; :: thesis: (0. K,n,m) * i,j = 0. K

then [i,j] in [:(Seg n),(Seg m):] by A1, MATRIX_1:24;
then A3: ( i in Seg n & j in Seg m ) by ZFMISC_1:106;
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
A4: (0. K,n,m) . i = m |-> (0. K) by A3, FUNCOP_1:13;
(m1 |-> (0. K)) . j = 0. K by A3, FUNCOP_1:13;
hence (0. K,n,m) * i,j = 0. K by A1, A4, MATRIX_1:def 6; :: thesis: verum

end;

suppose n = 0 ; :: thesis: (0. K,n,m) * i,j = 0. K

hence (0. K,n,m) * i,j = 0. K by A1, A2, FINSEQ_1:4, ZFMISC_1:113; :: thesis: verum

end;

end;