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