let
f
,
g
be
complex-valued
Function
;
:: thesis:
for
r
being
Complex
holds
r
(#)
(
g
/
f
)
=
(
r
(#)
g
)
/
f
let
r
be
Complex
;
:: thesis:
r
(#)
(
g
/
f
)
=
(
r
(#)
g
)
/
f
thus
r
(#)
(
g
/
f
)
=
r
(#)
(
g
(#)
(
f
^
)
)
by
Th31
.=
(
r
(#)
g
)
(#)
(
f
^
)
by
Th12
.=
(
r
(#)
g
)
/
f
by
Th31
;
:: thesis:
verum