let z, z3 be quaternion number ; :: thesis: ( z is Real implies z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*] )
assume z is Real ; :: thesis: z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*]
then reconsider x = z as Real ;
a: ( Rea z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )

proof

B2: x = [*x,0 *] by ARYTM_0:def 7;
[*x,0 *] = [*x,0 ,0 ,0 *] by QUATERNI:def 6;
hence ( Rea z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by B2, QUATERNI:23; :: thesis: verum

end;

z * z3 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*]

proof

set z1 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*];
reconsider z' = z * z3 as quaternion number ;
A1: Rea [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3)) by QUATERNI:23
.= Rea z' by Lm2 ;
A2: Im1 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3)) by QUATERNI:23
.= Im1 z' by Lm2 ;
A3: Im2 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3)) by QUATERNI:23
.= Im2 z' by Lm2 ;
Im3 [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] = ((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)) by QUATERNI:23
.= Im3 z' by Lm2 ;
hence z * z3 = [*(((((Rea z) * (Rea z3)) - ((Im1 z) * (Im1 z3))) - ((Im2 z) * (Im2 z3))) - ((Im3 z) * (Im3 z3))),(((((Rea z) * (Im1 z3)) + ((Im1 z) * (Rea z3))) + ((Im2 z) * (Im3 z3))) - ((Im3 z) * (Im2 z3))),(((((Rea z) * (Im2 z3)) + ((Im2 z) * (Rea z3))) + ((Im3 z) * (Im1 z3))) - ((Im1 z) * (Im3 z3))),(((((Rea z) * (Im3 z3)) + ((Im3 z) * (Rea z3))) + ((Im1 z) * (Im2 z3))) - ((Im2 z) * (Im1 z3)))*] by A1, A2, A3, QUATERNI:25; :: thesis: verum

end;

hence z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*] by a; :: thesis: verum