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