let n be Nat; for K being Field
for a being Element of K holds ((n,n) --> a) @ = (n,n) --> a
let K be Field; for a being Element of K holds ((n,n) --> a) @ = (n,n) --> a
let a be Element of K; ((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;
( [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) @)
;
(((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;
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; verum