let X be non empty TopSpace; for f, g being continuous Function of the carrier of X,COMPLEX holds f (#) g is continuous Function of the carrier of X,COMPLEX
let f, g be continuous Function of the carrier of X,COMPLEX; f (#) g is continuous Function of the carrier of X,COMPLEX
set h = f (#) g;
A1:
for x being Point of X holds (f (#) g) . x = (f . x) * (g . x)
by VALUED_1:5;
for p being Point of X
for V being Subset of COMPLEX st (f (#) g) . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & (f (#) g) .: W c= V )
proof
let p be
Point of
X;
for V being Subset of COMPLEX st (f (#) g) . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & (f (#) g) .: W c= V )let V be
Subset of
COMPLEX;
( (f (#) g) . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & (f (#) g) .: W c= V ) )
assume A2:
(
(f (#) g) . p in V &
V is
open )
;
ex W being Subset of X st
( p in W & W is open & (f (#) g) .: W c= V )
reconsider z0 =
(f (#) g) . p as
Complex ;
consider N being
Neighbourhood of
z0 such that A3:
N c= V
by A2, CFDIFF_1:9;
consider r being
Real such that A4:
(
0 < r &
{ y where y is Complex : |.(y - z0).| < r } c= N )
by CFDIFF_1:def 5;
set S =
{ y where y is Complex : |.(y - z0).| < r } ;
reconsider z1 =
f . p as
Complex ;
reconsider z2 =
g . p as
Complex ;
set a =
(|.z1.| + |.z2.|) + 1;
set S1 =
{ y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } ;
{ y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } c= COMPLEX
then reconsider T1 =
{ y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } as
Subset of
COMPLEX ;
A5:
T1 is
open
by CFDIFF_1:13;
|.(z1 - z1).| = 0
;
then
z1 in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) }
by A4;
then consider W1 being
Subset of
X such that A6:
(
p in W1 &
W1 is
open &
f .: W1 c= { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } )
by A5, Th3;
set S2 =
{ y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } ;
{ y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } c= COMPLEX
then reconsider T2 =
{ y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } as
Subset of
COMPLEX ;
A7:
T2 is
open
by CFDIFF_1:13;
|.(z2 - z2).| = 0
;
then
z2 in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) }
by A4;
then consider W2 being
Subset of
X such that A8:
(
p in W2 &
W2 is
open &
g .: W2 c= { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } )
by A7, Th3;
reconsider jj = 1 as
Real ;
set S3 =
{ y where y is Complex : |.(y - z1).| < jj } ;
{ y where y is Complex : |.(y - z1).| < jj } c= COMPLEX
then reconsider T3 =
{ y where y is Complex : |.(y - z1).| < jj } as
Subset of
COMPLEX ;
A9:
T3 is
open
by CFDIFF_1:13;
|.(z1 - z1).| = 0
;
then
z1 in { y where y is Complex : |.(y - z1).| < jj }
;
then consider W3 being
Subset of
X such that A10:
(
p in W3 &
W3 is
open &
f .: W3 c= { y where y is Complex : |.(y - z1).| < jj } )
by A9, Th3;
set W =
(W1 /\ W2) /\ W3;
W1 /\ W2 is
open
by A6, A8, TOPS_1:11;
then A11:
(W1 /\ W2) /\ W3 is
open
by A10, TOPS_1:11;
p in W1 /\ W2
by A6, A8, XBOOLE_0:def 4;
then A12:
p in (W1 /\ W2) /\ W3
by A10, XBOOLE_0:def 4;
(f (#) g) .: ((W1 /\ W2) /\ W3) c= { y where y is Complex : |.(y - z0).| < r }
proof
let z3 be
object ;
TARSKI:def 3 ( not z3 in (f (#) g) .: ((W1 /\ W2) /\ W3) or z3 in { y where y is Complex : |.(y - z0).| < r } )
assume
z3 in (f (#) g) .: ((W1 /\ W2) /\ W3)
;
z3 in { y where y is Complex : |.(y - z0).| < r }
then consider x3 being
object such that A13:
(
x3 in dom (f (#) g) &
x3 in (W1 /\ W2) /\ W3 &
(f (#) g) . x3 = z3 )
by FUNCT_1:def 6;
A14:
x3 in W1 /\ W2
by A13, XBOOLE_0:def 4;
then A15:
x3 in W1
by XBOOLE_0:def 4;
reconsider px =
x3 as
Point of
X by A13;
A16:
px in the
carrier of
X
;
then
px in dom f
by FUNCT_2:def 1;
then
f . px in f .: W1
by A15, FUNCT_1:def 6;
then A17:
f . px in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) }
by A6;
reconsider a1 =
f . px as
Complex ;
ex
aa1 being
Complex st
(
f . px = aa1 &
|.(aa1 - z1).| < r / ((|.z1.| + |.z2.|) + 1) )
by A17;
then A18:
|.(a1 - z1).| < r / ((|.z1.| + |.z2.|) + 1)
;
A19:
x3 in W2
by A14, XBOOLE_0:def 4;
px in dom g
by A16, FUNCT_2:def 1;
then
g . px in g .: W2
by A19, FUNCT_1:def 6;
then A20:
g . px in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) }
by A8;
reconsider a2 =
g . px as
Complex ;
ex
aa2 being
Complex st
(
g . px = aa2 &
|.(aa2 - z2).| < r / ((|.z1.| + |.z2.|) + 1) )
by A20;
then A21:
|.(a2 - z2).| < r / ((|.z1.| + |.z2.|) + 1)
;
A22:
x3 in W3
by A13, XBOOLE_0:def 4;
px in dom f
by A16, FUNCT_2:def 1;
then
f . px in f .: W3
by A22, FUNCT_1:def 6;
then A23:
f . px in { y where y is Complex : |.(y - z1).| < jj }
by A10;
reconsider a3 =
f . px as
Complex ;
ex
aa3 being
Complex st
(
f . px = aa3 &
|.(aa3 - z1).| < 1 )
by A23;
then A24:
|.(a3 - z1).| < 1
;
|.((a1 - z1) + z1).| <= |.(a1 - z1).| + |.z1.|
by COMPLEX1:56;
then
|.a1.| - |.z1.| <= (|.(a1 - z1).| + |.z1.|) - |.z1.|
by XREAL_1:9;
then
|.a1.| - |.z1.| < 1
by A24, XXREAL_0:2;
then
(|.a1.| - |.z1.|) + |.z1.| < 1
+ |.z1.|
by XREAL_1:8;
then A25:
|.a1.| < 1
+ |.z1.|
;
A26:
|.(((f (#) g) . x3) - z0).| =
|.(((f . px) * (g . px)) - z0).|
by A1
.=
|.((a1 * a2) - (z1 * z2)).|
by A1
.=
|.(((a1 * a2) - (a1 * z2)) + ((a1 * z2) - (z1 * z2))).|
;
A27:
|.(((f (#) g) . x3) - z0).| <= |.((a1 * a2) - (a1 * z2)).| + |.((a1 * z2) - (z1 * z2)).|
by A26, COMPLEX1:56;
|.((a1 * a2) - (a1 * z2)).| + |.((a1 * z2) - (z1 * z2)).| =
|.(a1 * (a2 - z2)).| + |.(z2 * (a1 - z1)).|
.=
(|.a1.| * |.(a2 - z2).|) + |.(z2 * (a1 - z1)).|
by COMPLEX1:65
.=
(|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|)
by COMPLEX1:65
;
then A28:
|.(((f (#) g) . x3) - z0).| <= (|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|)
by A27;
A29:
|.a1.| * |.(a2 - z2).| <= |.a1.| * (r / ((|.z1.| + |.z2.|) + 1))
by A21, XREAL_1:66;
|.a1.| * (r / ((|.z1.| + |.z2.|) + 1)) < (1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))
by A25, A4, XREAL_1:68;
then A30:
|.a1.| * |.(a2 - z2).| < (1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))
by A29, XXREAL_0:2;
A31:
|.z2.| * |.(a1 - z1).| <= |.z2.| * (r / ((|.z1.| + |.z2.|) + 1))
by A18, XREAL_1:66;
A32:
(|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) < ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * |.(a1 - z1).|)
by A30, XREAL_1:8;
((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * |.(a1 - z1).|) <= ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * (r / ((|.z1.| + |.z2.|) + 1)))
by A31, XREAL_1:6;
then
(|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) < ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * (r / ((|.z1.| + |.z2.|) + 1)))
by A32, XXREAL_0:2;
then A33:
|.(((f (#) g) . x3) - z0).| < r * (((|.z1.| + |.z2.|) + 1) / ((|.z1.| + |.z2.|) + 1))
by A28, XXREAL_0:2;
((|.z1.| + |.z2.|) + 1) / ((|.z1.| + |.z2.|) + 1) = 1
by XCMPLX_0:def 7;
then
|.(((f (#) g) . px) - z0).| < r
by A33;
hence
z3 in { y where y is Complex : |.(y - z0).| < r }
by A13;
verum
end;
then
(f (#) g) .: ((W1 /\ W2) /\ W3) c= N
by A4;
hence
ex
W being
Subset of
X st
(
p in W &
W is
open &
(f (#) g) .: W c= V )
by A11, A12, A3, XBOOLE_1:1;
verum
end;
hence
f (#) g is continuous Function of the carrier of X,COMPLEX
by Th3; verum