theorem Th53: :: BKMODEL1:61

for ra being non zero Real
for N, O, M being Matrix of 3,3,REAL st N is invertible & M = ra * O & M = ((N @) * O) * N holds
(((Inv N) @) * O) * (Inv N) = (1 / ra) * O