let z be Quaternion; :: thesis: 2 * (Rea z) = Rea (z + (z *'))
( z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] & z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] ) by QUATERNI:24, QUATERNI:43;
then z + (z *') = [*((Rea z) + (Rea z)),((Im1 z) + (- (Im1 z))),((Im2 z) + (- (Im2 z))),((Im3 z) + (- (Im3 z)))*] by QUATERNI:def 7
.= [*(2 * (Rea z)),0,0,0*] ;
hence 2 * (Rea z) = Rea (z + (z *')) by QUATERNI:23; :: thesis: verum