let a be Real; :: thesis: for p, q being Rational st a > 0 holds
(a #Q p) #Q q = a #Q (p * q)

let p, q be Rational; :: thesis: ( a > 0 implies (a #Q p) #Q q = a #Q (p * q) )
A1: denominator p >= 1 by RAT_1:11;
p = () / () by RAT_1:15;
then p * q = (() / ()) * (() / ()) by RAT_1:15
.= ((() / ()) * ()) / ()
.= (() * ()) / (() * ()) by XCMPLX_1:83 ;
then consider n being Nat such that
A2: (numerator p) * () = (numerator (p * q)) * n and
A3: (denominator p) * () = (denominator (p * q)) * n by RAT_1:27;
A4: (denominator (p * q)) * n >= 0 + 1 by ;
n > 0 by A3;
then A5: n >= 0 + 1 by NAT_1:13;
reconsider k = n as Integer ;
A6: denominator q >= 1 by RAT_1:11;
A7: denominator (p * q) >= 1 by RAT_1:11;
assume A8: a > 0 ; :: thesis: (a #Q p) #Q q = a #Q (p * q)
then A9: a #Z (() * ()) >= 0 by Th39;
A10: a #Q (p * q) > 0 by ;
A11: a #Z (numerator (p * q)) > 0 by ;
a #Z () > 0 by ;
hence (a #Q p) #Q q = () -Root (() -Root ((a #Z ()) #Z ())) by
.= () -Root (() -Root (a #Z (() * ()))) by Th45
.= ((denominator (p * q)) * n) -Root (a #Z ((numerator (p * q)) * k)) by A1, A6, A9, A2, A3, Th25
.= ((denominator (p * q)) * n) -Root ((a #Z (numerator (p * q))) #Z k) by Th45
.= (((denominator (p * q)) * n) -Root (a #Z (numerator (p * q)))) #Z k by
.= ((n * (denominator (p * q))) -Root (a #Z (numerator (p * q)))) |^ n by Th36
.= (n -Root (a #Q (p * q))) |^ n by A5, A7, A11, Th25
.= a #Q (p * q) by A5, A10, Lm2 ;
:: thesis: verum