let a, b, c be Real; :: thesis: ( a > 0 & b > 0 implies (a / b) #R c = (a #R c) / (b #R c) )
assume that
A1: a > 0 and
A2: b > 0 ; :: thesis: (a / b) #R c = (a #R c) / (b #R c)
thus (a / b) #R c = (a * (b ")) #R c
.= (a #R c) * ((b ") #R c) by A1, A2, Th78
.= (a #R c) * ((1 / b) #R c)
.= (a #R c) * (1 / (b #R c)) by A2, Th79
.= ((a #R c) * 1) / (b #R c)
.= (a #R c) / (b #R c) ; :: thesis: verum