for n being Nat
for K being Field
for a being Element of K holds ((n,n) --> a) @ = (n,n) --> a