reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
defpred S₁[ set , set , set ] means ( ( $1 = $2 implies $3 = 1. K ) & ( $1 <> $2 implies $3 = 0. K ) );
A1: for i, j being Nat st [i,j] in [:(Seg n1),(Seg n1):] holds
for x1, x2 being Element of K st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 ;
A2: for i, j being Nat st [i,j] in [:(Seg n1),(Seg n1):] holds
ex x being Element of K st S₁[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 S₁[i,j,x] )
assume [i,j] in [:(Seg n1),(Seg n1):] ; :: thesis: ex x being Element of K st S₁[i,j,x]
( ( i = j implies S₁[i,j, 1. K] ) & ( i <> j implies S₁[i,j, 0. K] ) ) ;
hence ex x being Element of K st S₁[i,j,x] ; :: thesis: verum

end;

consider M being Matrix of n1,K such that
A3: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * i,j] from MATRIX_1:sch 2(A1, A2);
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 A3; :: thesis: verum