theorem :: MATRIX_6:58

for n being Nat
for K being Field holds 1. (K,n) is Orthogonal