let z be Quaternion; :: thesis: ( Rea (z * (z *')) = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) & Im1 (z * (z *')) = 0 & Im2 (z * (z *')) = 0 & Im3 (z * (z *')) = 0 )
A1: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by Th17;
z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Th36;
then z * (z *') = [*(((((Rea z) * (Rea z)) - ((Im1 z) * (- (Im1 z)))) - ((Im2 z) * (- (Im2 z)))) - ((Im3 z) * (- (Im3 z)))),(((((Rea z) * (- (Im1 z))) + ((Im1 z) * (Rea z))) + ((Im2 z) * (- (Im3 z)))) - ((Im3 z) * (- (Im2 z)))),(((((Rea z) * (- (Im2 z))) + ((Rea z) * (Im2 z))) + ((- (Im1 z)) * (Im3 z))) - ((- (Im3 z)) * (Im1 z))),(((((Rea z) * (- (Im3 z))) + ((Im3 z) * (Rea z))) + ((Im1 z) * (- (Im2 z)))) - ((Im2 z) * (- (Im1 z))))*] by A1, Def9
.= [*(((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)),0,0,0*] ;
hence ( Rea (z * (z *')) = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) & Im1 (z * (z *')) = 0 & Im2 (z * (z *')) = 0 & Im3 (z * (z *')) = 0 ) by Th16; :: thesis: verum