let z be Quaternion; :: thesis: ( Rea (z * z) = ((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2) & Im1 (z * z) = 2 * ((Rea z) * (Im1 z)) & Im2 (z * z) = 2 * ((Rea z) * (Im2 z)) & Im3 (z * z) = 2 * ((Rea z) * (Im3 z)) )
( Rea (z * z) = ((((Rea z) * (Rea z)) - ((Im1 z) * (Im1 z))) - ((Im2 z) * (Im2 z))) - ((Im3 z) * (Im3 z)) & Im1 (z * z) = ((((Rea z) * (Im1 z)) + ((Im1 z) * (Rea z))) + ((Im2 z) * (Im3 z))) - ((Im3 z) * (Im2 z)) & Im2 (z * z) = ((((Rea z) * (Im2 z)) + ((Im2 z) * (Rea z))) + ((Im3 z) * (Im1 z))) - ((Im1 z) * (Im3 z)) & Im3 (z * z) = ((((Rea z) * (Im3 z)) + ((Im3 z) * (Rea z))) + ((Im1 z) * (Im2 z))) - ((Im2 z) * (Im1 z)) ) by Lm17;
hence ( Rea (z * z) = ((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2) & Im1 (z * z) = 2 * ((Rea z) * (Im1 z)) & Im2 (z * z) = 2 * ((Rea z) * (Im2 z)) & Im3 (z * z) = 2 * ((Rea z) * (Im3 z)) ) ; :: thesis: verum