( Rea 0q = 0 & Im1 0q = 0 & Im2 0q = 0 & Im3 0q = 0 ) by Lm5, Th23;
hence |.0q .| = 0 by SQUARE_1:82; :: thesis: verum