theorem Th43: :: MATRIX_6:42

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