let a, b, c be Real; :: thesis: ( a > 0 implies a #R (b - c) = (a #R b) / (a #R c) )
assume A1: a > 0 ; :: thesis: a #R (b - c) = (a #R b) / (a #R c)
thus a #R (b - c) = a #R (b + (- c))
.= (a #R b) * (a #R (- c)) by A1, Th75
.= (a #R b) * (1 / (a #R c)) by A1, Th76
.= (a #R b) * (1 * ((a #R c) "))
.= (a #R b) / (a #R c) ; :: thesis: verum