A1: Rea 1q = jj by Lm10, Th16;
A2: Im1 1q = zz by Lm10, Th16;
Im2 1q = zz by Lm10, Th16;
hence |.1q.| = 1 by A1, A2, Lm10, Th16, SQUARE_1:18; :: thesis: verum