let z3, z be Quaternion; :: thesis: ( z is Real implies z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * <i>)) + ((Im2 z3) * <j>)) + ((Im3 z3) * <k>) )
reconsider z1 = z + z3 as Quaternion ;
assume A1: z is Real ; :: thesis: z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * <i>)) + ((Im2 z3) * <j>)) + ((Im3 z3) * <k>)
then A2: Im3 z = 0 by Lm1;
set z2 = [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*];
A3: Rea [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Rea z) + (Rea z3) by QUATERNI:23
.= Rea z1 by QUATERNI:36 ;
A4: Im1 [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Im1 z) + (Im1 z3) by QUATERNI:23
.= Im1 z1 by QUATERNI:36 ;
A5: Im3 [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Im3 z) + (Im3 z3) by QUATERNI:23
.= Im3 z1 by QUATERNI:36 ;
A6: Im2 [*((Rea z) + (Rea z3)),((Im1 z) + (Im1 z3)),((Im2 z) + (Im2 z3)),((Im3 z) + (Im3 z3))*] = (Im2 z) + (Im2 z3) by QUATERNI:23
.= Im2 z1 by QUATERNI:36 ;
( Im1 z = 0 & Im2 z = 0 ) by A1, Lm1;
then z + z3 = [*((Rea z) + (Rea z3)),(Im1 z3),(Im2 z3),(Im3 z3)*] by A2, A3, A4, A6, A5, QUATERNI:25;
hence z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * <i>)) + ((Im2 z3) * <j>)) + ((Im3 z3) * <k>) by QUATERN2:1; :: thesis: verum