let z be quaternion number ; ( Rea (z - (z *')) = 0 & Im1 (z - (z *')) = 2 * (Im1 z) & Im2 (z - (z *')) = 2 * (Im2 z) & Im3 (z - (z *')) = 2 * (Im3 z) )
A1:
z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]
by Th24;
A2:
z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]
by Th43;
A4:
Im1 (z *') = - (Im1 z)
by A2, Th23;
A5:
Im2 (z *') = - (Im2 z)
by A2, Th23;
AA:
Im3 (z *') = - (Im3 z)
by A2, Th23;
set zz = z *' ;
- (z *') = [*(- (Rea (z *'))),(- (Im1 (z *'))),(- (Im2 (z *'))),(- (Im3 (z *')))*]
by Th62;
then
- (z *') = [*(- (Rea z)),(Im1 z),(Im2 z),(Im3 z)*]
by A2, Th23, A4, A5, AA;
then z - (z *') =
[*((Rea z) + (- (Rea z))),((Im1 z) + (Im1 z)),((Im2 z) + (Im2 z)),((Im3 z) + (Im3 z))*]
by A1, Def7
.=
[*0,(2 * (Im1 z)),(2 * (Im2 z)),(2 * (Im3 z))*]
;
hence
( Rea (z - (z *')) = 0 & Im1 (z - (z *')) = 2 * (Im1 z) & Im2 (z - (z *')) = 2 * (Im2 z) & Im3 (z - (z *')) = 2 * (Im3 z) )
by Th23; verum