let z1, z2 be quaternion number ; 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 z9 = 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 z9
by Lm13
;
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 z9
by Lm13
;
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 z9
by Lm13
;
Im3 [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] =
(Im3 z1) + (Im3 z2)
by Th23
.=
Im3 z9
by Lm13
;
hence
z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*]
by A1, A2, A3, Th25; verum