let z be Element of R_Quaternion; :: thesis: - z = (- (1_ R_Quaternion)) * z
reconsider z9 = z as Element of QUATERNION by Def10;
thus - z = (- 1q) * z9 by Th19
.= (- (1_ R_Quaternion)) * z by Def10 ; :: thesis: verum