let z, z3 be quaternion number ; :: thesis: ( z is Real implies z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*] )
assume z is Real ; :: thesis: z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*]
then reconsider x = z as Real ;
a: ( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )

proof

B2: x = [*x,0 *] by ARYTM_0:def 7;
[*x,0 *] = [*x,0 ,0 ,0 *] by QUATERNI:def 6;
hence ( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by B2, QUATERNI:23; :: thesis: verum

end;

set z2 = [*((Rea z) - (Rea z3)),((Im1 z) - (Im1 z3)),((Im2 z) - (Im2 z3)),((Im3 z) - (Im3 z3))*];
reconsider z1 = z + (- z3) as quaternion number ;
A1: 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 ;
A2: 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 ;
A3: 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 ;
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 ;
hence z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*] by A1, A2, A3, a, QUATERNI:25; :: thesis: verum