defpred S_{1}[ 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_{1}[i,j,x]

A2: for i, j being Nat st [i,j] in Indices M holds

S_{1}[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

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

proof

consider M being Matrix of n1,K such that
let i, j be Nat; :: thesis: ( [i,j] in [:(Seg n1),(Seg n1):] implies ex x being Element of K st S_{1}[i,j,x] )

assume [i,j] in [:(Seg n1),(Seg n1):] ; :: thesis: ex x being Element of K st S_{1}[i,j,x]

( i = j implies S_{1}[i,j, 1. K] )
;

hence ex x being Element of K st S_{1}[i,j,x]
; :: thesis: verum

end;assume [i,j] in [:(Seg n1),(Seg n1):] ; :: thesis: ex x being Element of K st S

( i = j implies S

hence ex x being Element of K st S

A2: for i, j being Nat st [i,j] in Indices M holds

S

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