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 = 1. 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 = 1. K
let l, j be Nat; :: thesis: ( [l,j] in Indices (1. (K,n)) & l = j implies (Col ((1. (K,n)),j)) . l = 1. K )
assume that
A1: [l,j] in Indices (1. (K,n)) and
A2: l = j ; :: thesis: (Col ((1. (K,n)),j)) . l = 1. 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
.= 1. K by A1, A2, MATRIX_1:def 3 ;
:: thesis: verum