let a, b be Real; :: thesis: for p being Rational st a > 0 & b > 0 holds
(a / b) #Q p = (a #Q p) / (b #Q p)
let p be Rational; :: thesis: ( a > 0 & b > 0 implies (a / b) #Q p = (a #Q p) / (b #Q p) )
assume that
A1: a > 0 and
A2: b > 0 ; :: thesis: (a / b) #Q p = (a #Q p) / (b #Q p)
thus (a / b) #Q p = (a * (1 / b)) #Q p
.= (a #Q p) * ((1 / b) #Q p) by A1, A2, Th56
.= (a #Q p) * (1 / (b #Q p)) by A2, Th57
.= (a #Q p) / (b #Q p) ; :: thesis: verum