theorem Th20: :: MATRIX_6:20

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