let n be Nat; :: thesis: for K being Ring
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 Ring; :: 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
l in Seg (width (1. (K,n))) by A1, ZFMISC_1:87;
hence (Line ((1. (K,n)),i)) . l = (1. (K,n)) * (i,l) by MATRIX_0:def 7
.= 0. K by A1, A2, MATRIX_1:def 3 ;
:: thesis: verum