let n, m be Nat; :: thesis: for K being Ring
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 Ring; :: 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_0:25;
per cases ( n > 0 or n = 0 ) ;
suppose A3: n > 0 ; :: thesis: (0. (K,n,m)) * (i,j) = 0. K
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
A4: [i,j] in [:(Seg n),(Seg m):] by A1, A3, MATRIX_0:23;
then j in Seg m by ZFMISC_1:87;
then A5: (m1 |-> (0. K)) . j = 0. K by FUNCOP_1:7;
i in Seg n by A4, ZFMISC_1:87;
then (0. (K,n,m)) . i = m |-> (0. K) by FUNCOP_1:7;
hence (0. (K,n,m)) * (i,j) = 0. K by A1, A5, MATRIX_0:def 5; :: thesis: verum
end;
suppose n = 0 ; :: thesis: (0. (K,n,m)) * (i,j) = 0. K
then Seg n = {} ;
hence (0. (K,n,m)) * (i,j) = 0. K by A1, A2, ZFMISC_1:90; :: thesis: verum
end;
end;