let p, q, a, b be Real; :: thesis: ( 1 < p & (1 / p) + (1 / q) = 1 & 0 < a & 0 < b implies ( a * b <= ((a #R p) / p) + ((b #R q) / q) & ( a * b = ((a #R p) / p) + ((b #R q) / q) implies a #R p = b #R q ) & ( a #R p = b #R q implies a * b = ((a #R p) / p) + ((b #R q) / q) ) ) )
assume that
A1: 1 < p and
A2: (1 / p) + (1 / q) = 1 and
A3: 0 < a and
A4: 0 < b ; :: thesis: ( a * b <= ((a #R p) / p) + ((b #R q) / q) & ( a * b = ((a #R p) / p) + ((b #R q) / q) implies a #R p = b #R q ) & ( a #R p = b #R q implies a * b = ((a #R p) / p) + ((b #R q) / q) ) )
A5: 0 < b #R q by A4, PREPOWER:95;
reconsider pp = 1 / p as Real ;
1 - pp <> 0 by A1, XREAL_1:191;
then A6: (q " ) " <> 0 by A2;
then (((1 * q) + (1 * p)) / (p * q)) * (p * q) = 1 * (p * q) by A1, A2, XCMPLX_1:117;
then A7: q + p = p * q by A1, A6, XCMPLX_1:6, XCMPLX_1:88;
then A8: (q - 1) * p = q ;
A9: 0 < b #R (q - 1) by A4, PREPOWER:95;

A10: now

assume A11: a #R p = b #R q ; :: thesis: ((a #R p) / p) + ((b #R q) / q) = a * b
then A12: a #R p = (b #R (q - 1)) #R p by A4, A8, PREPOWER:105;
a = a #R 1 by A3, PREPOWER:86
.= a #R (p * (1 / p)) by A1, XCMPLX_1:107
.= (a #R p) #R (1 / p) by A3, PREPOWER:105
.= (b #R (q - 1)) #R (p * (1 / p)) by A4, A12, PREPOWER:95, PREPOWER:105
.= (b #R (q - 1)) #R 1 by A1, XCMPLX_1:107
.= b #R (q - 1) by A4, PREPOWER:86, PREPOWER:95 ;
then a * 1 = b #R (q - 1) ;
then a * (b #R ((1 - q) + (q - 1))) = b #R (q - 1) by A4, PREPOWER:85;
then a * ((b #R (1 - q)) * (b #R (q - 1))) = 1 * (b #R (q - 1)) by A4, PREPOWER:89;
then A13: (a * (b #R (1 - q))) * (b #R (q - 1)) = 1 * (b #R (q - 1)) ;
thus ((a #R p) / p) + ((b #R q) / q) = ((b #R q) * (1 / p)) + ((b #R q) / q) by A11, XCMPLX_1:100
.= ((b #R q) * (1 / p)) + ((b #R q) * (1 / q)) by XCMPLX_1:100
.= (b #R q) * ((1 / p) + (1 / q))
.= (b #R q) * (a * (b #R (1 - q))) by A2, A9, A13, XCMPLX_1:5
.= a * ((b #R (1 - q)) * (b #R q))
.= a * (b #R ((1 - q) + q)) by A4, PREPOWER:89
.= a * b by A4, PREPOWER:86 ; :: thesis: verum

end;

A14: 0 < b #R (1 - q) by A4, PREPOWER:95;
then A15: 0 * (b #R (1 - q)) < a * (b #R (1 - q)) by A3, XREAL_1:70;
ex h being PartFunc of REAL ,REAL st
( dom h = right_open_halfline 0 & ( for x being Real st x > 0 holds
( h . x = (x #R p) / p & h is_differentiable_in x & diff h,x = x #R (p - 1) ) ) )

proof

set h = (1 / p) (#) (#R p);
take (1 / p) (#) (#R p) ; :: thesis: ( dom ((1 / p) (#) (#R p)) = right_open_halfline 0 & ( for x being Real st x > 0 holds
( ((1 / p) (#) (#R p)) . x = (x #R p) / p & (1 / p) (#) (#R p) is_differentiable_in x & diff ((1 / p) (#) (#R p)),x = x #R (p - 1) ) ) )
dom (#R p) = right_open_halfline 0 by TAYLOR_1:def 4;
hence A16: dom ((1 / p) (#) (#R p)) = right_open_halfline 0 by VALUED_1:def 5; :: thesis: for x being Real st x > 0 holds
( ((1 / p) (#) (#R p)) . x = (x #R p) / p & (1 / p) (#) (#R p) is_differentiable_in x & diff ((1 / p) (#) (#R p)),x = x #R (p - 1) )

now

let x be Real; :: thesis: ( x > 0 implies ( ((1 / p) (#) (#R p)) . x = (x #R p) / p & (1 / p) (#) (#R p) is_differentiable_in x & diff ((1 / p) (#) (#R p)),x = x #R (p - 1) ) )
assume A17: x > 0 ; :: thesis: ( ((1 / p) (#) (#R p)) . x = (x #R p) / p & (1 / p) (#) (#R p) is_differentiable_in x & diff ((1 / p) (#) (#R p)),x = x #R (p - 1) )
x in { g where g is Real : 0 < g } by A17;
then A18: x in right_open_halfline 0 by XXREAL_1:230;
hence ((1 / p) (#) (#R p)) . x = (1 / p) * ((#R p) . x) by A16, VALUED_1:def 5
.= (1 / p) * (x #R p) by A18, TAYLOR_1:def 4
.= (x #R p) / p by XCMPLX_1:100 ;
:: thesis: ( (1 / p) (#) (#R p) is_differentiable_in x & diff ((1 / p) (#) (#R p)),x = x #R (p - 1) )
A19: #R p is_differentiable_in x by A17, TAYLOR_1:21;
hence (1 / p) (#) (#R p) is_differentiable_in x by FDIFF_1:23; :: thesis: diff ((1 / p) (#) (#R p)),x = x #R (p - 1)
thus diff ((1 / p) (#) (#R p)),x = (1 / p) * (diff (#R p),x) by A19, FDIFF_1:23
.= (1 / p) * (p * (x #R (p - 1))) by A17, TAYLOR_1:21
.= ((1 / p) * p) * (x #R (p - 1))
.= 1 * (x #R (p - 1)) by A1, XCMPLX_1:107
.= x #R (p - 1) ; :: thesis: verum

end;

hence for x being Real st x > 0 holds
( ((1 / p) (#) (#R p)) . x = (x #R p) / p & (1 / p) (#) (#R p) is_differentiable_in x & diff ((1 / p) (#) (#R p)),x = x #R (p - 1) ) ; :: thesis: verum

end;

then consider h being PartFunc of REAL ,REAL such that
A20: dom h = right_open_halfline 0 and
A21: for x being Real st x > 0 holds
( h . x = (x #R p) / p & h is_differentiable_in x & diff h,x = x #R (p - 1) ) ;
ex g being PartFunc of REAL ,REAL st
( dom g = REAL & ( for x being Real holds
( g . x = (1 / q) - x & ( for x being Real holds
( g is_differentiable_in x & diff g,x = - 1 ) ) ) ) )

proof

deffunc H₁( Real) -> Element of REAL = (1 / q) - $1;
defpred S₁[ set ] means $1 in REAL ;
consider g being PartFunc of REAL ,REAL such that
A22: for d being Element of REAL holds
( d in dom g iff S₁[d] ) and
A23: for d being Element of REAL st d in dom g holds
g /. d = H₁(d) from PARTFUN2:sch 2();
take g ; :: thesis: ( dom g = REAL & ( for x being Real holds
( g . x = (1 / q) - x & ( for x being Real holds
( g is_differentiable_in x & diff g,x = - 1 ) ) ) ) )
for x being set st x in REAL holds
x in dom g by A22;
then A24: ( dom g c= REAL & REAL c= dom g ) by RELAT_1:def 18, TARSKI:def 3;
then A25: dom g = [#] REAL by XBOOLE_0:def 10;
A26: for d being Element of REAL holds g . d = (1 / q) - d

proof

let d be Element of REAL ; :: thesis: g . d = (1 / q) - d
g /. d = (1 / q) - d by A23, A25;
hence g . d = (1 / q) - d by A25, PARTFUN1:def 8; :: thesis: verum

end;

A27: for d being Real st d in REAL holds
g . d = ((- 1) * d) + (1 / q)

proof

let d be Real; :: thesis: ( d in REAL implies g . d = ((- 1) * d) + (1 / q) )
assume d in REAL ; :: thesis: g . d = ((- 1) * d) + (1 / q)
thus g . d = (1 / q) - d by A26
.= ((- 1) * d) + (1 / q) ; :: thesis: verum

end;

then A28: g is_differentiable_on dom g by A25, FDIFF_1:31;
for x being Real holds
( g is_differentiable_in x & diff g,x = - 1 )

proof

let d be Real; :: thesis: ( g is_differentiable_in d & diff g,d = - 1 )
thus g is_differentiable_in d by A25, A28, FDIFF_1:16; :: thesis: diff g,d = - 1
thus diff g,d = (g `| (dom g)) . d by A25, A28, FDIFF_1:def 8
.= - 1 by A25, A27, FDIFF_1:31 ; :: thesis: verum

end;

hence ( dom g = REAL & ( for x being Real holds
( g . x = (1 / q) - x & ( for x being Real holds
( g is_differentiable_in x & diff g,x = - 1 ) ) ) ) ) by A24, A26, XBOOLE_0:def 10; :: thesis: verum

end;

then consider g being PartFunc of REAL ,REAL such that
A29: dom g = REAL and
A30: for x being Real holds g . x = (1 / q) - x and
A31: for x being Real holds
( g is_differentiable_in x & diff g,x = - 1 ) ;
set f = h + g;
A32: dom (h + g) = (right_open_halfline 0 ) /\ REAL by A29, A20, VALUED_1:def 1
.= right_open_halfline 0 by XBOOLE_1:28 ;
A33: for x being Real st x in right_open_halfline 0 holds
( (h + g) . x = (((x #R p) / p) + (1 / q)) - x & h + g is_differentiable_in x & diff (h + g),x = (x #R (p - 1)) - 1 )

proof

let x be Real; :: thesis: ( x in right_open_halfline 0 implies ( (h + g) . x = (((x #R p) / p) + (1 / q)) - x & h + g is_differentiable_in x & diff (h + g),x = (x #R (p - 1)) - 1 ) )
assume A34: x in right_open_halfline 0 ; :: thesis: ( (h + g) . x = (((x #R p) / p) + (1 / q)) - x & h + g is_differentiable_in x & diff (h + g),x = (x #R (p - 1)) - 1 )
x in { y where y is Real : 0 < y } by A34, XXREAL_1:230;
then A35: ex y being Real st
( x = y & 0 < y ) ;
then A36: diff h,x = x #R (p - 1) by A21;
thus (h + g) . x = (h . x) + (g . x) by A32, A34, VALUED_1:def 1
.= ((x #R p) / p) + (g . x) by A21, A35
.= ((x #R p) / p) + ((1 / q) - x) by A30
.= (((x #R p) / p) + (1 / q)) - x ; :: thesis: ( h + g is_differentiable_in x & diff (h + g),x = (x #R (p - 1)) - 1 )
A37: g is_differentiable_in x by A31;
A38: h is_differentiable_in x by A21, A35;
hence h + g is_differentiable_in x by A37, FDIFF_1:21; :: thesis: diff (h + g),x = (x #R (p - 1)) - 1
A39: diff g,x = - 1 by A31;
thus diff (h + g),x = (diff h,x) + (diff g,x) by A37, A38, FDIFF_1:21
.= (x #R (p - 1)) - 1 by A39, A36 ; :: thesis: verum

end;

A40: for x being Real st 0 < x & x <> 1 holds
x < ((x #R p) / p) + (1 / q)

proof

1 in { y where y is Real : 0 < y } ;
then 1 in right_open_halfline 0 by XXREAL_1:230;
then A41: (h + g) . 1 = (((1 #R p) / p) + (1 / q)) - 1 by A33
.= ((1 / p) + (1 / q)) - 1 by PREPOWER:87
.= 0 by A2 ;
for x being Real st x in right_open_halfline 0 holds
h + g is_differentiable_in x by A33;
then A42: h + g is_differentiable_on right_open_halfline 0 by A32, FDIFF_1:16;
let x be Real; :: thesis: ( 0 < x & x <> 1 implies x < ((x #R p) / p) + (1 / q) )
assume that
A43: 0 < x and
A44: x <> 1 ; :: thesis: x < ((x #R p) / p) + (1 / q)
x in { y where y is Real : 0 < y } by A43;
then A45: x in right_open_halfline 0 by XXREAL_1:230;

now

per cases ( x < 1 or x > 1 ) by A44, XXREAL_0:1;

case x < 1 ; :: thesis: x < ((x #R p) / p) + (1 / q)

then A46: 1 - 1 < 1 - x by XREAL_1:17;
set t = 1 - x;
A47: 1 - 1 < p - 1 by A1, XREAL_1:16;

now

let z be set ; :: thesis: ( z in [.x,(x + (1 - x)).] implies z in right_open_halfline 0 )
assume z in [.x,(x + (1 - x)).] ; :: thesis: z in right_open_halfline 0
then z in { r where r is Real : ( x <= r & r <= x + (1 - x) ) } by RCOMP_1:def 1;
then ex r being Real st
( r = z & x <= r & r <= x + (1 - x) ) ;
then z in { y where y is Real : 0 < y } by A43;
hence z in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum

end;

then A48: [.x,(x + (1 - x)).] c= right_open_halfline 0 by TARSKI:def 3;
(h + g) | (right_open_halfline 0 ) is continuous by A42, FDIFF_1:33;
then A49: (h + g) | [.x,(x + (1 - x)).] is continuous by A48, FCONT_1:17;
].x,(x + (1 - x)).[ c= [.x,(x + (1 - x)).] by XXREAL_1:25;
then h + g is_differentiable_on ].x,(x + (1 - x)).[ by A42, A48, FDIFF_1:34, XBOOLE_1:1;
then consider s being Real such that
A50: 0 < s and
A51: s < 1 and
A52: (h + g) . (x + (1 - x)) = ((h + g) . x) + ((1 - x) * (diff (h + g),(x + (s * (1 - x))))) by A32, A46, A48, A49, ROLLE:4;
s * (1 - x) < 1 * (1 - x) by A46, A51, XREAL_1:70;
then x + (s * (1 - x)) < x + (1 - x) by XREAL_1:10;
then (x + (s * (1 - x))) to_power (p - 1) < (x + (s * (1 - x))) to_power 0 by A43, A46, A50, A47, POWER:45;
then (x + (s * (1 - x))) #R (p - 1) < (x + (s * (1 - x))) to_power 0 by A43, A46, A50, POWER:def 2;
then (x + (s * (1 - x))) #R (p - 1) < (x + (s * (1 - x))) #R 0 by A43, A46, A50, POWER:def 2;
then (x + (s * (1 - x))) #R (p - 1) < 1 by A43, A46, A50, PREPOWER:85;
then A53: ((x + (s * (1 - x))) #R (p - 1)) - 1 < 1 - 1 by XREAL_1:16;
x + (s * (1 - x)) in { y where y is Real : 0 < y } by A43, A46, A50;
then x + (s * (1 - x)) in right_open_halfline 0 by XXREAL_1:230;
then diff (h + g),(x + (s * (1 - x))) = ((x + (s * (1 - x))) #R (p - 1)) - 1 by A33;
then (1 - x) * (diff (h + g),(x + (s * (1 - x)))) < (1 - x) * 0 by A46, A53, XREAL_1:70;
then ((h + g) . x) + ((1 - x) * (diff (h + g),(x + (s * (1 - x))))) < ((h + g) . x) + 0 by XREAL_1:10;
then 0 < (((x #R p) / p) + (1 / q)) - x by A33, A45, A41, A52;
then 0 + x < ((((x #R p) / p) + (1 / q)) - x) + x by XREAL_1:10;
hence x < ((x #R p) / p) + (1 / q) ; :: thesis: verum

end;

case x > 1 ; :: thesis: x < ((x #R p) / p) + (1 / q)

then A54: 1 - 1 < x - 1 by XREAL_1:16;
set t = x - 1;

now

let z be set ; :: thesis: ( z in [.1,(1 + (x - 1)).] implies z in right_open_halfline 0 )
assume z in [.1,(1 + (x - 1)).] ; :: thesis: z in right_open_halfline 0
then z in { r where r is Real : ( 1 <= r & r <= 1 + (x - 1) ) } by RCOMP_1:def 1;
then ex r being Real st
( r = z & 1 <= r & r <= 1 + (x - 1) ) ;
then z in { y where y is Real : 0 < y } ;
hence z in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum

end;

then A55: [.1,(1 + (x - 1)).] c= right_open_halfline 0 by TARSKI:def 3;
A56: 1 - 1 < p - 1 by A1, XREAL_1:16;
(h + g) | (right_open_halfline 0 ) is continuous by A42, FDIFF_1:33;
then A57: (h + g) | [.1,(1 + (x - 1)).] is continuous by A55, FCONT_1:17;
].1,(1 + (x - 1)).[ c= [.1,(1 + (x - 1)).] by XXREAL_1:25;
then h + g is_differentiable_on ].1,(1 + (x - 1)).[ by A42, A55, FDIFF_1:34, XBOOLE_1:1;
then consider s being Real such that
A58: 0 < s and
s < 1 and
A59: (h + g) . (1 + (x - 1)) = ((h + g) . 1) + ((x - 1) * (diff (h + g),(1 + (s * (x - 1))))) by A32, A54, A55, A57, ROLLE:4;
0 * (x - 1) < s * (x - 1) by A54, A58, XREAL_1:70;
then 1 + 0 < 1 + (s * (x - 1)) by XREAL_1:10;
then 1 < (1 + (s * (x - 1))) #R (p - 1) by A56, PREPOWER:100;
then A60: 1 - 1 < ((1 + (s * (x - 1))) #R (p - 1)) - 1 by XREAL_1:16;
1 + (s * (x - 1)) in { y where y is Real : 0 < y } by A54, A58;
then 1 + (s * (x - 1)) in right_open_halfline 0 by XXREAL_1:230;
then diff (h + g),(1 + (s * (x - 1))) = ((1 + (s * (x - 1))) #R (p - 1)) - 1 by A33;
then (x - 1) * 0 < (x - 1) * (diff (h + g),(1 + (s * (x - 1)))) by A54, A60, XREAL_1:70;
then 0 < (((x #R p) / p) + (1 / q)) - x by A33, A45, A41, A59;
then 0 + x < ((((x #R p) / p) + (1 / q)) - x) + x by XREAL_1:10;
hence x < ((x #R p) / p) + (1 / q) ; :: thesis: verum

end;

end;

end;

hence x < ((x #R p) / p) + (1 / q) ; :: thesis: verum

end;

A61: ((1 - q) * p) + q = 0 by A7;

A62: now

assume a * b = ((a #R p) / p) + ((b #R q) / q) ; :: thesis: a #R p = b #R q
then a * b = ((a #R p) / p) + ((1 / q) * (b #R q)) by XCMPLX_1:100;
then a * b = ((a #R p) * (1 / p)) + ((1 / q) * (b #R q)) by XCMPLX_1:100;
then a * b = ((a #R p) * ((b #R 0 ) / p)) + ((1 / q) * (b #R q)) by A4, PREPOWER:85;
then a * b = ((a #R p) * (((b #R ((1 - q) * p)) * (b #R q)) / p)) + ((1 / q) * (b #R q)) by A4, A61, PREPOWER:89;
then a * b = ((a #R p) * (((b #R ((1 - q) * p)) / p) * (b #R q))) + ((1 / q) * (b #R q)) by XCMPLX_1:75;
then a * b = (((a #R p) * ((b #R ((1 - q) * p)) / p)) * (b #R q)) + ((1 / q) * (b #R q)) ;
then a * b = ((((a #R p) * (b #R ((1 - q) * p))) / p) * (b #R q)) + ((1 / q) * (b #R q)) by XCMPLX_1:75;
then a * b = ((((a #R p) * (b #R ((1 - q) * p))) / p) + (1 / q)) * (b #R q) ;
then a * b = ((((a #R p) * ((b #R (1 - q)) #R p)) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:105;
then a * b = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A3, A14, PREPOWER:92;
then a * (b #R ((1 - q) + q)) = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:86;
then a * ((b #R (1 - q)) * (b #R q)) = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:89;
then (a * (b #R (1 - q))) * (b #R q) = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) ;
then A63: a * (b #R (1 - q)) = (((a * (b #R (1 - q))) #R p) / p) + (1 / q) by A5, XCMPLX_1:5;
a * ((b #R (1 - q)) * (b #R (q - 1))) = (a * (b #R (1 - q))) * (b #R (q - 1))
.= 1 * (b #R (q - 1)) by A40, A15, A63 ;
then a * (b #R ((1 - q) + (q - 1))) = b #R (q - 1) by A4, PREPOWER:89;
then a * 1 = b #R (q - 1) by A4, PREPOWER:85;
hence a #R p = b #R q by A4, A8, PREPOWER:105; :: thesis: verum

end;

a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q)

proof

now

per cases ( a * (b #R (1 - q)) = 1 or a * (b #R (1 - q)) <> 1 ) ;

case a * (b #R (1 - q)) = 1 ; :: thesis: a * (b #R (1 - q)) = (((a * (b #R (1 - q))) #R p) / p) + (1 / q)

hence a * (b #R (1 - q)) = (((a * (b #R (1 - q))) #R p) / p) + (1 / q) by A2, PREPOWER:87; :: thesis: verum

end;

case a * (b #R (1 - q)) <> 1 ; :: thesis: a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q)

hence a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q) by A40, A15; :: thesis: verum

end;

end;

end;

hence a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q) ; :: thesis: verum

end;

then (a * (b #R (1 - q))) * (b #R q) <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A5, XREAL_1:66;
then a * ((b #R (1 - q)) * (b #R q)) <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) ;
then a * (b #R ((1 - q) + q)) <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:89;
then a * b <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:86;
then a * b <= ((((a #R p) * ((b #R (1 - q)) #R p)) / p) + (1 / q)) * (b #R q) by A3, A14, PREPOWER:92;
then a * b <= ((((a #R p) * (b #R ((1 - q) * p))) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:105;
then a * b <= ((((a #R p) * (b #R ((1 - q) * p))) / p) * (b #R q)) + ((1 / q) * (b #R q)) ;
then a * b <= (((a #R p) * ((b #R ((1 - q) * p)) / p)) * (b #R q)) + ((1 / q) * (b #R q)) by XCMPLX_1:75;
then a * b <= ((a #R p) * (((b #R ((1 - q) * p)) / p) * (b #R q))) + ((1 / q) * (b #R q)) ;
then a * b <= ((a #R p) * (((b #R ((1 - q) * p)) * (b #R q)) / p)) + ((1 / q) * (b #R q)) by XCMPLX_1:75;
then a * b <= ((a #R p) * ((b #R (((1 - q) * p) + q)) / p)) + ((1 / q) * (b #R q)) by A4, PREPOWER:89;
then a * b <= ((a #R p) * (1 / p)) + ((1 / q) * (b #R q)) by A4, A7, PREPOWER:85;
then a * b <= ((a #R p) / p) + ((1 / q) * (b #R q)) by XCMPLX_1:100;
hence ( a * b <= ((a #R p) / p) + ((b #R q) / q) & ( a * b = ((a #R p) / p) + ((b #R q) / q) implies a #R p = b #R q ) & ( a #R p = b #R q implies a * b = ((a #R p) / p) + ((b #R q) / q) ) ) by A62, A10, XCMPLX_1:100; :: thesis: verum