let n be Nat; for K being Ring
for l, j being Nat st [l,j] in Indices (1. (K,n)) & l <> j holds
(Col ((1. (K,n)),j)) . l = 0. K
let K be Ring; for l, j being Nat st [l,j] in Indices (1. (K,n)) & l <> j holds
(Col ((1. (K,n)),j)) . l = 0. K
let l, j be Nat; ( [l,j] in Indices (1. (K,n)) & l <> j implies (Col ((1. (K,n)),j)) . l = 0. K )
assume that
A1:
[l,j] in Indices (1. (K,n))
and
A2:
l <> j
; (Col ((1. (K,n)),j)) . l = 0. K
l in dom (1. (K,n))
by A1, ZFMISC_1:87;
hence (Col ((1. (K,n)),j)) . l =
(1. (K,n)) * (l,j)
by MATRIX_0:def 8
.=
0. K
by A1, A2, MATRIX_1:def 3
;
verum