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