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