defpred S1[ set , set , set ] means ( ( \$1 = \$2 implies \$3 = 1. K ) & ( \$1 <> \$2 implies \$3 = 0. K ) );
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
A1: for i, j being Nat st [i,j] in [:(Seg n1),(Seg n1):] holds
ex x being Element of K st S1[i,j,x]
proof
let i, j be Nat; :: thesis: ( [i,j] in [:(Seg n1),(Seg n1):] implies ex x being Element of K st S1[i,j,x] )
assume [i,j] in [:(Seg n1),(Seg n1):] ; :: thesis: ex x being Element of K st S1[i,j,x]
( i = j implies S1[i,j, 1. K] ) ;
hence ex x being Element of K st S1[i,j,x] ; :: thesis: verum
end;
consider M being Matrix of n1,K such that
A2: for i, j being Nat st [i,j] in Indices M holds
S1[i,j,M * (i,j)] from reconsider M = M as Matrix of n,K ;
take M ; :: thesis: ( ( for i being Nat st [i,i] in Indices M holds
M * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M & i <> j holds
M * (i,j) = 0. K ) )

thus ( ( for i being Nat st [i,i] in Indices M holds
M * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices M & i <> j holds
M * (i,j) = 0. K ) ) by A2; :: thesis: verum