theorem :: QUATERN2:40

for z being Element of R_Quaternion holds - z = (- (1_ R_Quaternion)) * z