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;
( [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):]
;
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]
;
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 MATRIX_0:sch 2(A1);
reconsider M = M as Matrix of n,K ;
take
M
; ( ( 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; verum