let z3, z be Quaternion; ( z is Real implies z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*] )
reconsider z1 = z + (- z3) as Quaternion ;
assume A1:
z is Real
; z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*]
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 z) + (Rea (- z3))
by QUATERNI:41
.=
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 z) + (Im1 (- z3))
by QUATERNI:41
.=
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 z) + (Im3 (- z3))
by QUATERNI:41
.=
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 z) + (Im2 (- z3))
by QUATERNI:41
.=
Im2 z1
by QUATERNI:36
;
( Im1 z = 0 & Im2 z = 0 )
by A1, Lm1;
hence
z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*]
by A2, A3, A4, A6, A5, QUATERNI:25; verum