let a, b be real number ; :: 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 A1: ( a > 0 & b > 0 ) ; :: thesis: (a * b) #Q p = (a #Q p) * (b #Q p)
then A2: a #Z (numerator p) >= 0 by Th49;
A3: b #Z (numerator p) >= 0 by A1, Th49;
thus (a * b) #Q p = (denominator p) -Root ((a #Z (numerator p)) * (b #Z (numerator p))) by Th50
.= (a #Q p) * (b #Q p) by A2, A3, Th31, RAT_1:29 ; :: thesis: verum