let n be Nat; :: thesis: for R being Ring
for a being Element of R holds ((n,n) --> a) @ = (n,n) --> a
let R be Ring; :: thesis: for a being Element of R holds ((n,n) --> a) @ = (n,n) --> a
let a be Element of R; :: thesis: ((n,n) --> a) @ = (n,n) --> a
len ((n,n) --> a) = n by MATRIX_0:24;
then A1: len (((n,n) --> a) @) = len ((n,n) --> a) by MATRIX_0:24;
A2: Indices ((n,n) --> a) = [:(Seg n),(Seg n):] by MATRIX_0: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_0: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_0:46, MATRIX_0:def 6;
hence (((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (i,j) by A4, MATRIX_0:46; :: thesis: verum

end;

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