reconsider z' = [*(- v),(- w),(- x),(- y)*] as quaternion number ;
take z' ; :: thesis: z + z' = 0
( 0 = v + (- v) & 0 = w + (- w) & 0 = x + (- x) & 0 = y + (- y) ) ;
hence z + z' = 0 by A1, Def7, Lm5; :: thesis: verum