let
x
be
Real
;
:: thesis:
for
q
being
Rational
holds
(
exp_R
x
)
#R
q
=
exp_R
(
q
*
x
)
let
q
be
Rational
;
:: thesis:
(
exp_R
x
)
#R
q
=
exp_R
(
q
*
x
)
ex
m
being
Integer
ex
n
being
Nat
st
(
n
<>
0
&
q
=
m
/
n
)
by
RAT_1:8
;
hence
(
exp_R
x
)
#R
q
=
exp_R
(
q
*
x
)
by
Th6
;
:: thesis:
verum