let n be Nat; :: thesis: for K being Field
for a being Element of K holds n,n --> a is symmetric
let K be Field; :: thesis: for a being Element of K holds n,n --> a is symmetric
let a be Element of K; :: thesis: n,n --> a is symmetric
(n,n --> a) @ = n,n --> a by Th21;
hence n,n --> a is symmetric by Def5; :: thesis: verum