let c be Quaternion; :: thesis: (- c) " = - (c ")
A1: 1q = [*jj,(In (0,REAL))*] by ARYTM_0:def 5
.= [*1,0,0,0*] by QUATERNI:91 ;
consider x1, x2, x3, x4 being Element of REAL such that
A2: c = [*x1,x2,x3,x4*] by Lm1;
A3: - c = [*(- x1),(- x2),(- x3),(- x4)*] by A2, Th4;
A4: |.(- c).| = |.c.| by QUATERNI:72;
A5: c " = [*(((((x1 * 1) + (x2 * 0)) + (x3 * 0)) + (x4 * 0)) / (|.c.| ^2)),(((((x1 * 0) - (x2 * 1)) - (x3 * 0)) + (x4 * 0)) / (|.c.| ^2)),(((((x1 * 0) + (x2 * 0)) - (x3 * 1)) - (x4 * 0)) / (|.c.| ^2)),(((((x1 * 0) - (x2 * 0)) + (x3 * 0)) - (x4 * jj)) / (|.c.| ^2))*] by A1, A2, Def1, Lm5
.= [*(x1 / (|.c.| ^2)),(- (x2 / (|.c.| ^2))),(- (x3 / (|.c.| ^2))),(- (x4 / (|.c.| ^2)))*] ;
(- c) " = [*((((((- x1) * 1) + ((- x2) * 0)) + ((- x3) * 0)) + ((- x4) * 0)) / (|.(- c).| ^2)),((((((- x1) * 0) - ((- x2) * 1)) - ((- x3) * 0)) + ((- x4) * 0)) / (|.(- c).| ^2)),((((((- x1) * 0) + ((- x2) * 0)) - ((- x3) * 1)) - ((- x4) * 0)) / (|.(- c).| ^2)),((((((- x1) * 0) - ((- x2) * 0)) + ((- x3) * 0)) - ((- x4) * jj)) / (|.(- c).| ^2))*] by A1, A3, Def1, Lm5
.= [*(- (x1 / (|.c.| ^2))),(x2 / (|.c.| ^2)),(x3 / (|.c.| ^2)),(x4 / (|.c.| ^2))*] by A4 ;
then (c ") + ((- c) ") = [*((x1 / (|.c.| ^2)) + (- (x1 / (|.c.| ^2)))),((- (x2 / (|.c.| ^2))) + (x2 / (|.c.| ^2))),((- (x3 / (|.c.| ^2))) + (x3 / (|.c.| ^2))),((- (x4 / (|.c.| ^2))) + (x4 / (|.c.| ^2)))*] by A5, QUATERNI:def 7
.= [*(In (0,REAL)),(In (0,REAL))*] by QUATERNI:91
.= 0 by ARYTM_0:def 5 ;
hence (- c) " = - (c ") by QUATERNI:def 8; :: thesis: verum