let x1, x2, x3, x4 be Real; :: thesis: [*x1,x2,x3,x4*] *' = [*x1,(- x2),(- x3),(- x4)*]
set c = [*x1,x2,x3,x4*];
A1: Rea [*x1,x2,x3,x4*] = x1 by QUATERNI:23;
A2: Im1 [*x1,x2,x3,x4*] = x2 by QUATERNI:23;
A3: Im2 [*x1,x2,x3,x4*] = x3 by QUATERNI:23;
Im3 [*x1,x2,x3,x4*] = x4 by QUATERNI:23;
hence [*x1,x2,x3,x4*] *' = [*x1,(- x2),(- x3),(- x4)*] by A1, A2, A3, QUATERNI:43; :: thesis: verum