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

(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