let z be Quaternion; ( Rea (z + (z *')) = 2 * (Rea z) & 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)))*]
by A1, Def6
.=
[*(2 * (Rea z)),0,0,0*]
;
hence
( Rea (z + (z *')) = 2 * (Rea z) & Im1 (z + (z *')) = 0 & Im2 (z + (z *')) = 0 & Im3 (z + (z *')) = 0 )
by Th16; verum