let a, c be real number ; :: thesis: ( a > 0 implies (1 / a) #R c = 1 / (a #R c) )
assume A1: a > 0 ; :: thesis: (1 / a) #R c = 1 / (a #R c)
1 = 1 #R c by Th87
.= ((1 / a) * a) #R c by A1, XCMPLX_1:106
.= ((1 / a) #R c) * (a #R c) by A1, Th92 ;
then 1 / (a #R c) = ((1 / a) #R c) * ((a #R c) / (a #R c)) by XCMPLX_1:74
.= ((1 / a) #R c) * 1 by A1, Lm9, XCMPLX_1:60 ;
hence (1 / a) #R c = 1 / (a #R c) ; :: thesis: verum