let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( [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 ; :: thesis: (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 ;
:: thesis: verum