defpred S₁[ 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 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] ) ;
hence ex x being Element of K st S₁[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
S₁[i,j,M * (i,j)] from MATRIX_0:sch 2(A1);
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