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)

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 ; :: thesis: verum

(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)

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 ; :: thesis: verum