reconsider z9 = [*(- v),(- w),(- x),(- y)*] as Quaternion ;
take z9 ; :: thesis: z + z9 = 0
A2: 0 = v + (- v) ;
A3: 0 = w + (- w) ;
A4: 0 = x + (- x) ;
0 = y + (- y) ;
hence z + z9 = 0 by A1, A2, A3, A4, Def6, Lm6; :: thesis: verum