let z, z1, z2 be Quaternion; z1 - z2 = (z1 - z) + (z - z2)
A1: Rea ((z1 - z) + (z - z2)) =
(Rea (z1 - z)) + (Rea (z - z2))
by Lm12
.=
(Rea (z1 - z)) + ((Rea z) - (Rea z2))
by Th35
.=
((Rea z1) - (Rea z)) + ((Rea z) - (Rea z2))
by Th35
.=
(Rea z1) - (Rea z2)
.=
Rea (z1 - z2)
by Th35
;
A2: Im1 ((z1 - z) + (z - z2)) =
(Im1 (z1 - z)) + (Im1 (z - z2))
by Lm12
.=
(Im1 (z1 - z)) + ((Im1 z) - (Im1 z2))
by Th35
.=
((Im1 z1) - (Im1 z)) + ((Im1 z) - (Im1 z2))
by Th35
.=
(Im1 z1) - (Im1 z2)
.=
Im1 (z1 - z2)
by Th35
;
A3: Im2 ((z1 - z) + (z - z2)) =
(Im2 (z1 - z)) + (Im2 (z - z2))
by Lm12
.=
(Im2 (z1 - z)) + ((Im2 z) - (Im2 z2))
by Th35
.=
((Im2 z1) - (Im2 z)) + ((Im2 z) - (Im2 z2))
by Th35
.=
(Im2 z1) - (Im2 z2)
.=
Im2 (z1 - z2)
by Th35
;
Im3 ((z1 - z) + (z - z2)) =
(Im3 (z1 - z)) + (Im3 (z - z2))
by Lm12
.=
(Im3 (z1 - z)) + ((Im3 z) - (Im3 z2))
by Th35
.=
((Im3 z1) - (Im3 z)) + ((Im3 z) - (Im3 z2))
by Th35
.=
(Im3 z1) - (Im3 z2)
.=
Im3 (z1 - z2)
by Th35
;
hence
z1 - z2 = (z1 - z) + (z - z2)
by A1, A2, A3, Th18; verum