defpred S₁[ Nat, Nat, set ] means ( ( $1 = $2 implies $3 = L ) & ( $1 + 1 = $2 implies $3 = 1_ K ) & ( $1 <> $2 & $1 + 1 <> $2 implies $3 = 0. K ) );
reconsider N = n as Element of NAT by ORDINAL1:def 12;
A1: for i, j being Nat st [i,j] in [:(Seg N),(Seg N):] holds
ex x being Element of K st S₁[i,j,x]

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg N),(Seg N):] implies ex x being Element of K st S₁[i,j,x] )
assume [i,j] in [:(Seg N),(Seg N):] ; :: thesis: ex x being Element of K st S₁[i,j,x]

per cases ( i = j or i + 1 = j or ( i <> j & i + 1 <> j ) ) ;

suppose A2: i = j ; :: thesis: ex x being Element of K st S₁[i,j,x]

take L ; :: thesis: S₁[i,j,L]
thus S₁[i,j,L] by A2; :: thesis: verum

end;

suppose A3: i + 1 = j ; :: thesis: ex x being Element of K st S₁[i,j,x]

take 1_ K ; :: thesis: S₁[i,j, 1_ K]
thus S₁[i,j, 1_ K] by A3; :: thesis: verum

end;

suppose A4: ( i <> j & i + 1 <> j ) ; :: thesis: ex x being Element of K st S₁[i,j,x]

take 0. K ; :: thesis: S₁[i,j, 0. K]
thus S₁[i,j, 0. K] by A4; :: thesis: verum

end;

end;

end;

consider M being Matrix of N,K such that
A5: for i, j being Nat st [i,j] in Indices M holds
S₁[i,j,M * (i,j)] from MATRIX_0:sch 2(A1);
take M ; :: thesis: ( len M = n & width M = n & ( for i, j being Nat st [i,j] in Indices M holds
( ( i = j implies M * (i,j) = L ) & ( i + 1 = j implies M * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies M * (i,j) = 0. K ) ) ) )
thus ( len M = n & width M = n & ( for i, j being Nat st [i,j] in Indices M holds
( ( i = j implies M * (i,j) = L ) & ( i + 1 = j implies M * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies M * (i,j) = 0. K ) ) ) ) by A5, MATRIX_0:24; :: thesis: verum