theorem :: MATRIX_6:58

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