let z1, z2 be quaternion number ; :: thesis: z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*]
set z = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*];
reconsider z' = z1 + z2 as quaternion number ;
A1: Rea [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] = (Rea z1) + (Rea z2) by Th23
.= Rea z' by Lm11 ;
A2: Im1 [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] = (Im1 z1) + (Im1 z2) by Th23
.= Im1 z' by Lm11 ;
A3: Im2 [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] = (Im2 z1) + (Im2 z2) by Th23
.= Im2 z' by Lm11 ;
Im3 [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] = (Im3 z1) + (Im3 z2) by Th23
.= Im3 z' by Lm11 ;
hence z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] by A1, A2, A3, Th25; :: thesis: verum