let a, c be Real; :: thesis: ( a > 0 implies a #R (- c) = 1 / (a #R c) )
assume A1: a > 0 ; :: thesis: a #R (- c) = 1 / (a #R c)
then 1 = a #R (c + (- c)) by Th71
.= (a #R (- c)) * (a #R c) by A1, Th75 ;
then 1 / (a #R c) = (a #R (- c)) * ((a #R c) / (a #R c)) by XCMPLX_1:74
.= (a #R (- c)) * 1 by A1, Lm9, XCMPLX_1:60 ;
hence a #R (- c) = 1 / (a #R c) ; :: thesis: verum