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