let n be Nat; :: thesis: for K being Field
for i, l being Nat st [i,l] in Indices (1. K,n) & l <> i holds
(Line (1. K,n),i) . l = 0. K
let K be Field; :: thesis: for i, l being Nat st [i,l] in Indices (1. K,n) & l <> i holds
(Line (1. K,n),i) . l = 0. K
let i, l be Nat; :: thesis: ( [i,l] in Indices (1. K,n) & l <> i implies (Line (1. K,n),i) . l = 0. K )
assume that
A1: [i,l] in Indices (1. K,n) and
A2: l <> i ; :: thesis: (Line (1. K,n),i) . l = 0. K
Indices (1. K,n) = [:(dom (1. K,n)),(Seg (width (1. K,n))):] by MATRIX_1:def 5;
then l in Seg (width (1. K,n)) by A1, ZFMISC_1:106;
hence (Line (1. K,n),i) . l = (1. K,n) * i,l by MATRIX_1:def 8
.= 0. K by A1, A2, MATRIX_1:def 12 ;
:: thesis: verum