let X, Y be non empty TopSpace; :: thesis: for M being non empty set
for f being Function of M,the carrier of (oContMaps X,Y) holds commute f is continuous Function of X,(M -TOP_prod (M --> Y))
let M be non empty set ; :: thesis: for f being Function of M,the carrier of (oContMaps X,Y) holds commute f is continuous Function of X,(M -TOP_prod (M --> Y))
let f be Function of M,the carrier of (oContMaps X,Y); :: thesis: commute f is continuous Function of X,(M -TOP_prod (M --> Y))
A1:
( dom f = M & rng f c= the carrier of (oContMaps X,Y) )
by FUNCT_2:def 1;
the carrier of (oContMaps X,Y) c= Funcs the carrier of X,the carrier of Y
by Th33;
then
rng f c= Funcs the carrier of X,the carrier of Y
by XBOOLE_1:1;
then A2:
f in Funcs M,(Funcs the carrier of X,the carrier of Y)
by A1, FUNCT_2:def 2;
then
commute f in Funcs the carrier of X,(Funcs M,the carrier of Y)
by FUNCT_6:85;
then A3:
ex g being Function st
( commute f = g & dom g = the carrier of X & rng g c= Funcs M,the carrier of Y )
by FUNCT_2:def 2;
A4:
the carrier of (M -TOP_prod (M --> Y)) = product (Carrier (M --> Y))
by WAYBEL18:def 3;
A5:
Carrier (M --> Y) = M --> the carrier of Y
by Th31;
then
the carrier of (M -TOP_prod (M --> Y)) = Funcs M,the carrier of Y
by A4, CARD_3:20;
then reconsider g = commute f as Function of X,(M -TOP_prod (M --> Y)) by A3, FUNCT_2:4;
reconsider B = product_prebasis (M --> Y) as prebasis of M -TOP_prod (M --> Y) by WAYBEL18:def 3;
now let P be
Subset of
(M -TOP_prod (M --> Y));
:: thesis: ( P in B implies g " P is open )assume
P in B
;
:: thesis: g " P is open then consider i being
set ,
T being
TopStruct ,
V being
Subset of
T such that A6:
(
i in M &
V is
open &
T = (M --> Y) . i )
and A7:
P = product ((Carrier (M --> Y)) +* i,V)
by WAYBEL18:def 2;
A8:
T = Y
by A6, FUNCOP_1:13;
reconsider i =
i as
Element of
M by A6;
set FP =
(Carrier (M --> Y)) +* i,
V;
A9:
dom ((Carrier (M --> Y)) +* i,V) = dom (Carrier (M --> Y))
by FUNCT_7:32;
A10:
dom (Carrier (M --> Y)) = M
by A5, FUNCOP_1:19;
then A11:
((Carrier (M --> Y)) +* i,V) . i = V
by FUNCT_7:33;
reconsider fi =
f . i as
continuous Function of
X,
Y by Th2;
now let x be
set ;
:: thesis: ( ( x in g " P implies ex Q being Subset of X st
( Q is open & Q c= g " P & x in Q ) ) & ( ex Q being Subset of X st
( Q is open & Q c= g " P & x in Q ) implies x in g " P ) )hereby :: thesis: ( ex Q being Subset of X st
( Q is open & Q c= g " P & x in Q ) implies x in g " P )
assume A12:
x in g " P
;
:: thesis: ex Q being Subset of X st
( Q is open & Q c= g " P & x in Q )then
(
x in the
carrier of
X &
g . x in P )
by FUNCT_2:46;
then consider gx being
Function such that A13:
(
g . x = gx &
dom gx = dom ((Carrier (M --> Y)) +* i,V) & ( for
z being
set st
z in dom ((Carrier (M --> Y)) +* i,V) holds
gx . z in ((Carrier (M --> Y)) +* i,V) . z ) )
by A7, CARD_3:def 5;
reconsider Q =
fi " V as
Subset of
X ;
take Q =
Q;
:: thesis: ( Q is open & Q c= g " P & x in Q )
[#] Y <> {}
;
hence
Q is
open
by A6, A8, TOPS_2:55;
:: thesis: ( Q c= g " P & x in Q )thus
Q c= g " P
:: thesis: x in Qproof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in Q or a in g " P )
assume A14:
a in Q
;
:: thesis: a in g " P
then A15:
(
a in the
carrier of
X &
fi . a in V )
by FUNCT_2:46;
g . a in rng g
by A3, A14, FUNCT_1:def 5;
then consider ga being
Function such that A16:
(
g . a = ga &
dom ga = M &
rng ga c= the
carrier of
Y )
by A3, FUNCT_2:def 2;
now let z be
set ;
:: thesis: ( z in M implies ga . z in ((Carrier (M --> Y)) +* i,V) . z )assume A17:
z in M
;
:: thesis: ga . z in ((Carrier (M --> Y)) +* i,V) . zthen
( (
z <> i &
(M --> the carrier of Y) . z = the
carrier of
Y ) or
z = i )
by FUNCOP_1:13;
then
( (
z <> i &
ga . z in rng ga &
((Carrier (M --> Y)) +* i,V) . z = the
carrier of
Y ) or
z = i )
by A5, A16, A17, FUNCT_1:def 5, FUNCT_7:34;
hence
ga . z in ((Carrier (M --> Y)) +* i,V) . z
by A2, A11, A15, A16, FUNCT_6:86;
:: thesis: verum end;
then
ga in P
by A7, A9, A10, A16, CARD_3:18;
hence
a in g " P
by A14, A16, FUNCT_2:46;
:: thesis: verum
end; A18:
gx . i in V
by A9, A10, A11, A13;
gx . i = fi . x
by A2, A12, A13, FUNCT_6:86;
hence
x in Q
by A12, A18, FUNCT_2:46;
:: thesis: verum
end; thus
( ex
Q being
Subset of
X st
(
Q is
open &
Q c= g " P &
x in Q ) implies
x in g " P )
;
:: thesis: verum end; hence
g " P is
open
by TOPS_1:57;
:: thesis: verum end;
hence
commute f is continuous Function of X,(M -TOP_prod (M --> Y))
by YELLOW_9:36; :: thesis: verum