let a be Real; :: thesis: for p, q being Rational st a > 0 holds
(a #Q p) / (a #Q q) = a #Q (p - q)
let p, q be Rational; :: thesis: ( a > 0 implies (a #Q p) / (a #Q q) = a #Q (p - q) )
assume A1: a > 0 ; :: thesis: (a #Q p) / (a #Q q) = a #Q (p - q)
thus a #Q (p - q) = a #Q (p + (- q))
.= (a #Q p) * (a #Q (- q)) by A1, Th53
.= (a #Q p) * (1 / (a #Q q)) by A1, Th54
.= ((a #Q p) * 1) / (a #Q q)
.= (a #Q p) / (a #Q q) ; :: thesis: verum