let n be Nat; :: thesis: for K being Field holds (1. K,n) @ = 1. K,n
let K be Field; :: thesis: (1. K,n) @ = 1. K,n

per cases ( n > 0 or n = 0 ) by NAT_1:3;

suppose A1: n > 0 ; :: thesis: (1. K,n) @ = 1. K,n

A2: ( 1. K,n is Matrix of n,K & width (1. K,n) = n & len (1. K,n) = n ) by MATRIX_1:25;
then A3: ( len ((1. K,n) @ ) = width (1. K,n) & width ((1. K,n) @ ) = len (1. K,n) ) by A1, MATRIX_2:12;
A4: ( Indices ((1. K,n) @ ) = Indices (1. K,n) & Indices (1. K,n) = [:(Seg n),(Seg n):] ) by MATRIX_1:25, MATRIX_1:27;
for i, j being Nat st [i,j] in Indices (1. K,n) holds
(1. K,n) * i,j = ((1. K,n) @ ) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (1. K,n) implies (1. K,n) * i,j = ((1. K,n) @ ) * i,j )
assume [i,j] in Indices (1. K,n) ; :: thesis: (1. K,n) * i,j = ((1. K,n) @ ) * i,j
then ( i in Seg n & j in Seg n ) by A4, ZFMISC_1:106;
then A5: ( [i,j] in Indices (1. K,n) & [j,i] in Indices (1. K,n) ) by A4, ZFMISC_1:106;

per cases ( i = j or i <> j ) ;

suppose i = j ; :: thesis: (1. K,n) * i,j = ((1. K,n) @ ) * i,j

hence (1. K,n) * i,j = ((1. K,n) @ ) * i,j by A5, MATRIX_1:def 7; :: thesis: verum

end;

suppose i <> j ; :: thesis: (1. K,n) * i,j = ((1. K,n) @ ) * i,j

then ( (1. K,n) * i,j = 0. K & (1. K,n) * j,i = 0. K ) by A5, MATRIX_1:def 12;
hence (1. K,n) * i,j = ((1. K,n) @ ) * i,j by A5, MATRIX_1:def 7; :: thesis: verum

end;

end;

end;

hence (1. K,n) @ = 1. K,n by A2, A3, MATRIX_1:21; :: thesis: verum

end;

suppose n = 0 ; :: thesis: (1. K,n) @ = 1. K,n

hence (1. K,n) @ = 1. K,n by MATRIX_1:36; :: thesis: verum

end;

end;