let n be Nat; :: thesis: for K being Field
for a being Element of K holds ((n,n) --> a) @ = (n,n) --> a
let K be Field; :: thesis: for a being Element of K holds ((n,n) --> a) @ = (n,n) --> a
let a be Element of K; :: thesis: ((n,n) --> a) @ = (n,n) --> a
len ((n,n) --> a) = n by MATRIX_1:24;
then A1: len (((n,n) --> a) @) = len ((n,n) --> a) by MATRIX_1:24;
A2: Indices ((n,n) --> a) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A3: for i, j being Nat st [i,j] in Indices (((n,n) --> a) @) holds
(((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (((n,n) --> a) @) implies (((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (i,j) )
assume [i,j] in Indices (((n,n) --> a) @) ; :: thesis: (((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (i,j)
then A4: [i,j] in Indices ((n,n) --> a) by MATRIX_1:26;
then ( i in Seg n & j in Seg n ) by A2, ZFMISC_1:87;
then [j,i] in Indices ((n,n) --> a) by A2, ZFMISC_1:87;
then ( (((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (j,i) & ((n,n) --> a) * (j,i) = a ) by MATRIX_1:def 6, MATRIX_2:1;
hence (((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (i,j) by A4, MATRIX_2:1; :: thesis: verum

end;

width ((n,n) --> a) = n by MATRIX_1:24;
then width (((n,n) --> a) @) = width ((n,n) --> a) by MATRIX_1:24;
hence ((n,n) --> a) @ = (n,n) --> a by A1, A3, MATRIX_1:21; :: thesis: verum