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: len (1. K,n) = n by MATRIX_1:25;
A3: Indices (1. K,n) = [:(Seg n),(Seg n):] by MATRIX_1:25;
A4: 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 A5: [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 A3, ZFMISC_1:106;
then A6: [j,i] in Indices (1. K,n) by A3, 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, A6, MATRIX_1:def 12;
hence (1. K,n) * i,j = ((1. K,n) @ ) * i,j by A6, MATRIX_1:def 7; :: thesis: verum

end;

end;

end;

A7: width (1. K,n) = n by MATRIX_1:25;
then ( len ((1. K,n) @ ) = width (1. K,n) & width ((1. K,n) @ ) = len (1. K,n) ) by A1, MATRIX_2:12;
hence (1. K,n) @ = 1. K,n by A7, A2, A4, 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;