let n be Nat; :: thesis: for K being Field
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 Field; :: 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
Indices (1. K,n) = [:(dom (1. K,n)),(Seg (width (1. K,n))):] by MATRIX_1:def 5;
then l in dom (1. K,n) by A1, ZFMISC_1:106;
hence (Col (1. K,n),j) . l = (1. K,n) * l,j by MATRIX_1:def 9
.= 0. K by A1, A2, MATRIX_1:def 12 ;
:: thesis: verum