for n being Nat
for K being Field
for a being Element of K holds (n,n) --> a is symmetric by Th20;