let n be Nat; :: thesis: for K being Ring
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )
let K be Ring; :: thesis: for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )
let i, j be Nat; :: thesis: ( [i,j] in Indices (1. (K,n)) implies ( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) ) )
set B = 1. (K,n);
assume A1: [i,j] in Indices (1. (K,n)) ; :: thesis: ( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )
then j in Seg (width (1. (K,n))) by ZFMISC_1:87;
then A2: (Line ((1. (K,n)),i)) . j = (1. (K,n)) * (i,j) by MATRIX_0:def 7;
hence ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) by A1, MATRIX_1:def 3; :: thesis: ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K )
thus ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) by A1, A2, MATRIX_1:def 3; :: thesis: verum