theorem Th42: :: MATRIX_6:41

for n being Nat
for K being Ring
for M1 being Matrix of n,K holds
( ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) iff M1 is Orthogonal )