let R1, R2 be complex-valued Function; :: thesis: ( - R1 = - R2 implies R1 = R2 )
assume - R1 = - R2 ; :: thesis: R1 = R2
hence R1 = - (- R2)
.= R2 ;
:: thesis: verum