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;
A5:
r / ((|.z1.| + |.z2.|) + 1) is
Real
by XREAL_0:def 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 ;
A6:
T1 is
open
by CFDIFF_1:13, A5;
|.(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 A7:
(
p in W1 &
W1 is
open &
f .: W1 c= { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } )
by A6, 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 ;
A8:
T2 is
open
by CFDIFF_1:13, A5;
|.(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 A9:
(
p in W2 &
W2 is
open &
g .: W2 c= { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } )
by A8, Th3;
set S3 =
{ y where y is Complex : |.(y - z1).| < 1 } ;
{ y where y is Complex : |.(y - z1).| < 1 } c= COMPLEX
then reconsider T3 =
{ y where y is Complex : |.(y - z1).| < 1 } as
Subset of
COMPLEX ;
A10:
T3 is
open
by CFDIFF_1:13;
|.(z1 - z1).| = 0
;
then
z1 in { y where y is Complex : |.(y - z1).| < 1 }
;
then consider W3 being
Subset of
X such that A11:
(
p in W3 &
W3 is
open &
f .: W3 c= { y where y is Complex : |.(y - z1).| < 1 } )
by A10, Th3;
set W =
(W1 /\ W2) /\ W3;
W1 /\ W2 is
open
by A7, A9, TOPS_1:11;
then A12:
(W1 /\ W2) /\ W3 is
open
by A11, TOPS_1:11;
p in W1 /\ W2
by A7, A9, XBOOLE_0:def 4;
then A13:
p in (W1 /\ W2) /\ W3
by A11, XBOOLE_0:def 4;
(f (#) g) .: ((W1 /\ W2) /\ W3) c= { y where y is Complex : |.(y - z0).| < r }
proof
let z3 be
set ;
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
set such that A14:
(
x3 in dom (f (#) g) &
x3 in (W1 /\ W2) /\ W3 &
(f (#) g) . x3 = z3 )
by FUNCT_1:def 6;
A15:
x3 in W1 /\ W2
by A14, XBOOLE_0:def 4;
then A16:
x3 in W1
by XBOOLE_0:def 4;
reconsider px =
x3 as
Point of
X by A14;
A17:
px in the
carrier of
X
;
then
px in dom f
by FUNCT_2:def 1;
then
f . px in f .: W1
by A16, FUNCT_1:def 6;
then A18:
f . px in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) }
by A7;
reconsider a1 =
f . px as
Complex ;
ex
aa1 being
Complex st
(
f . px = aa1 &
|.(aa1 - z1).| < r / ((|.z1.| + |.z2.|) + 1) )
by A18;
then A19:
|.(a1 - z1).| < r / ((|.z1.| + |.z2.|) + 1)
;
A20:
x3 in W2
by XBOOLE_0:def 4, A15;
px in dom g
by A17, FUNCT_2:def 1;
then
g . px in g .: W2
by A20, FUNCT_1:def 6;
then A21:
g . px in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) }
by A9;
reconsider a2 =
g . px as
Complex ;
ex
aa2 being
Complex st
(
g . px = aa2 &
|.(aa2 - z2).| < r / ((|.z1.| + |.z2.|) + 1) )
by A21;
then A22:
|.(a2 - z2).| < r / ((|.z1.| + |.z2.|) + 1)
;
A23:
x3 in W3
by A14, XBOOLE_0:def 4;
px in dom f
by A17, FUNCT_2:def 1;
then
f . px in f .: W3
by A23, FUNCT_1:def 6;
then A24:
f . px in { y where y is Complex : |.(y - z1).| < 1 }
by A11;
reconsider a3 =
f . px as
Complex ;
ex
aa3 being
Complex st
(
f . px = aa3 &
|.(aa3 - z1).| < 1 )
by A24;
then A25:
|.(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 A25, XXREAL_0:2;
then
(|.a1.| - |.z1.|) + |.z1.| < 1
+ |.z1.|
by XREAL_1:8;
then A26:
|.a1.| < 1
+ |.z1.|
;
A27:
|.(((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))).|
;
A28:
|.(((f (#) g) . x3) - z0).| <= |.((a1 * a2) - (a1 * z2)).| + |.((a1 * z2) - (z1 * z2)).|
by A27, 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 A29:
|.(((f (#) g) . x3) - z0).| <= (|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|)
by A28;
A30:
|.a1.| * |.(a2 - z2).| <= |.a1.| * (r / ((|.z1.| + |.z2.|) + 1))
by A22, XREAL_1:66;
|.a1.| * (r / ((|.z1.| + |.z2.|) + 1)) < (1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))
by A26, A4, XREAL_1:68;
then A31:
|.a1.| * |.(a2 - z2).| < (1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))
by A30, XXREAL_0:2;
A32:
|.z2.| * |.(a1 - z1).| <= |.z2.| * (r / ((|.z1.| + |.z2.|) + 1))
by A19, XREAL_1:66;
A33:
(|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) < ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * |.(a1 - z1).|)
by A31, XREAL_1:8;
((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * |.(a1 - z1).|) <= ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * (r / ((|.z1.| + |.z2.|) + 1)))
by A32, XREAL_1:6;
then
(|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) < ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * (r / ((|.z1.| + |.z2.|) + 1)))
by A33, XXREAL_0:2;
then A34:
|.(((f (#) g) . x3) - z0).| < r * (((|.z1.| + |.z2.|) + 1) / ((|.z1.| + |.z2.|) + 1))
by A29, XXREAL_0:2;
((|.z1.| + |.z2.|) + 1) / ((|.z1.| + |.z2.|) + 1) = 1
by XCMPLX_0:def 7;
then
|.(((f (#) g) . px) - z0).| < r
by A34;
hence
z3 in { y where y is Complex : |.(y - z0).| < r }
by A14;
verum
end;
then
(f (#) g) .: ((W1 /\ W2) /\ W3) c= N
by A4, XBOOLE_1:1;
hence
ex
W being
Subset of
X st
(
p in W &
W is
open &
(f (#) g) .: W c= V )
by A12, A13, A3, XBOOLE_1:1;
verum
end;
hence
f (#) g is continuous Function of the carrier of X,COMPLEX
by Th3; verum