theorem
for
ra being non
zero Real for
O,
N,
M being
invertible Matrix of 3,
F_Real st
O = symmetric_3 (1,1,
(- 1),
0,
0,
0) &
M = symmetric_3 (
ra,
ra,
(- ra),
0,
0,
0) &
M = ((N @) * O) * N &
(homography M) .: absolute = absolute holds
(homography N) .: absolute = absolute