let a, b be Real; for p being Rational st a > 0 & b > 0 holds
(a * b) #Q p = (a #Q p) * (b #Q p)
let p be Rational; ( a > 0 & b > 0 implies (a * b) #Q p = (a #Q p) * (b #Q p) )
assume that
A1:
a > 0
and
A2:
b > 0
; (a * b) #Q p = (a #Q p) * (b #Q p)
A3:
a #Z (numerator p) >= 0
by A1, Th39;
A4:
b #Z (numerator p) >= 0
by A2, Th39;
thus (a * b) #Q p =
(denominator p) -Root ((a #Z (numerator p)) * (b #Z (numerator p)))
by Th40
.=
(a #Q p) * (b #Q p)
by A3, A4, Th22, RAT_1:11
; verum