let x, y, z be quaternion number ; :: thesis:
assume A1: z = x * y ; :: thesis:
consider x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL such that
A2: x = [*x1,x2,x3,x4*] and
A3: y = [*y1,y2,y3,y4*] and
A4: x * y = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] by QUATERNI:def 10;
A5: ( Rea x = x1 & Rea y = y1 ) by A2, A3, QUATERNI:23;
A6: ( Im1 x = x2 & Im1 y = y2 ) by A2, A3, QUATERNI:23;
A7: ( Im2 x = x3 & Im2 y = y3 ) by A2, A3, QUATERNI:23;
( Im3 x = x4 & Im3 y = y4 ) by A2, A3, QUATERNI:23;
hence ( Rea z = ((((Rea x) * (Rea y)) - ((Im1 x) * (Im1 y))) - ((Im2 x) * (Im2 y))) - ((Im3 x) * (Im3 y)) & Im1 z = ((((Rea x) * (Im1 y)) + ((Im1 x) * (Rea y))) + ((Im2 x) * (Im3 y))) - ((Im3 x) * (Im2 y)) & Im2 z = ((((Rea x) * (Im2 y)) + ((Im2 x) * (Rea y))) + ((Im3 x) * (Im1 y))) - ((Im1 x) * (Im3 y)) & Im3 z = ((((Rea x) * (Im3 y)) + ((Im3 x) * (Rea y))) + ((Im1 x) * (Im2 y))) - ((Im2 x) * (Im1 y)) ) by A1, A4, A5, A6, A7, QUATERNI:23; :: thesis: