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) )
set dp = denominator p;
set dq = denominator q;
set np = numerator p;
set nq = numerator q;
A1: denominator p >= 1 by RAT_1:11;
reconsider ddq = denominator q as Integer ;
reconsider ddp = denominator p as Integer ;
A2: denominator (p + q) >= 1 by RAT_1:11;
A3: denominator q >= 1 by RAT_1:11;
then A4: (denominator p) * () >= 1 by ;
p + q = (() / ()) + q by RAT_1:15
.= (() / ()) + (() / ()) by RAT_1:15
.= ((() * ()) + (() * ())) / (() * ()) by XCMPLX_1:116 ;
then consider n being Nat such that
A5: ((numerator p) * ()) + (() * ()) = (numerator (p + q)) * n and
A6: (denominator p) * () = (denominator (p + q)) * n by RAT_1:27;
reconsider k = n as Integer ;
assume A7: a > 0 ; :: thesis: (a #Q p) * (a #Q q) = a #Q (p + q)
then A8: a #Z (() - ()) >= 0 by Th39;
n > 0 by A6;
then A9: n >= 0 + 1 by NAT_1:13;
A10: a #Z () > 0 by ;
then A11: (a #Z ()) |^ (() + ()) >= 0 by Th6;
A12: a #Z (() - ()) > 0 by ;
then A13: (a #Z (() - ())) |^ () >= 0 by Th6;
A14: a #Q (p + q) > 0 by ;
A15: a #Z (numerator (p + q)) > 0 by ;
thus (a #Q p) * (a #Q q) = (() -Root (a #Z ())) * (() -Root (a #Z (() + (() - ()))))
.= (() -Root (a #Z ())) * (() -Root ((a #Z ()) * (a #Z (() - ())))) by
.= (() -Root (a #Z ())) * ((() -Root (a #Z ())) * (() -Root (a #Z (() - ())))) by
.= ((() -Root (a #Z ())) * (() -Root (a #Z ()))) * (() -Root (a #Z (() - ())))
.= ((() * ()) -Root ((a #Z ()) |^ (() + ()))) * (() -Root (a #Z (() - ()))) by A10, A3, A1, Th26
.= ((() * ()) -Root ((a #Z ()) |^ (() + ()))) * (() -Root (() -Root ((a #Z (() - ())) |^ ()))) by A12, A1, Lm2
.= ((() * ()) -Root ((a #Z ()) |^ (() + ()))) * ((() * ()) -Root ((a #Z (() - ())) |^ ())) by A3, A1, A13, Th25
.= (() * ()) -Root (((a #Z ()) |^ (() + ())) * ((a #Z (() - ())) |^ ())) by
.= (() * ()) -Root (((a #Z ()) #Z (ddp + ddq)) * ((a #Z (() - ())) |^ ())) by Th36
.= (() * ()) -Root (((a #Z ()) #Z (ddp + ddq)) * ((a #Z (() - ())) #Z ddp)) by Th36
.= (() * ()) -Root ((a #Z (() * (ddp + ddq))) * ((a #Z (() - ())) #Z ddp)) by Th45
.= (() * ()) -Root ((a #Z (() * (ddp + ddq))) * (a #Z ((() - ()) * ddp))) by Th45
.= (() * ()) -Root (a #Z (((() * ddp) + (() * ddq)) + ((() - ()) * ddp))) by
.= ((denominator (p + q)) * n) -Root ((a #Z (numerator (p + q))) #Z k) by A5, A6, Th45
.= (((denominator (p + q)) * n) -Root (a #Z (numerator (p + q)))) #Z k by A4, A6, A15, Th46
.= ((n * (denominator (p + q))) -Root (a #Z (numerator (p + q)))) |^ n by Th36
.= (n -Root (a #Q (p + q))) |^ n by A9, A2, A15, Th25
.= a #Q (p + q) by A9, A14, Lm2 ; :: thesis: verum