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))
reconsider B = product_prebasis (M --> Y) as prebasis of (M -TOP_prod (M --> Y)) by WAYBEL18:def 3;
A1: Carrier (M --> Y) = M --> the carrier of Y by Th30;
the carrier of (oContMaps (X,Y)) c= Funcs ( the carrier of X, the carrier of Y) by Th32;
then ( dom f = M & rng f c= Funcs ( the carrier of X, the carrier of Y) ) by FUNCT_2:def 1;
then A2: f in Funcs (M,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_2:def 2;
then commute f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) by FUNCT_6:55;
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;
the carrier of (M -TOP_prod (M --> Y)) = product (Carrier (M --> Y)) by WAYBEL18:def 3;
then the carrier of (M -TOP_prod (M --> Y)) = Funcs (M, the carrier of Y) by A1, CARD_3:11;
then reconsider g = commute f as Function of X,(M -TOP_prod (M --> Y)) by A3, FUNCT_2:2;

now :: thesis: for P being Subset of (M -TOP_prod (M --> Y)) st P in B holds
g " P is open

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
A4: i in M and
A5: V is open and
A6: T = (M --> Y) . i and
A7: P = product ((Carrier (M --> Y)) +* (i,V)) by WAYBEL18:def 2;
reconsider i = i as Element of M by A4;
set FP = (Carrier (M --> Y)) +* (i,V);
A8: dom ((Carrier (M --> Y)) +* (i,V)) = dom (Carrier (M --> Y)) by FUNCT_7:30;
reconsider fi = f . i as continuous Function of X,Y by Th2;
A9: dom (Carrier (M --> Y)) = M by A1, FUNCOP_1:13;
then A10: ((Carrier (M --> Y)) +* (i,V)) . i = V by FUNCT_7:31;
A11: T = Y by A4, A6, FUNCOP_1:7;

now :: thesis: for x being set holds
( ( 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 ) )

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 )

reconsider Q = fi " V as Subset of X ;
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 g . x in P by FUNCT_2:38;
then consider gx being Function such that
A13: g . x = gx and
dom gx = dom ((Carrier (M --> Y)) +* (i,V)) and
A14: for z being object 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;
A15: gx . i = fi . x by A2, A12, A13, FUNCT_6:56;
take Q = Q; :: thesis: ( Q is open & Q c= g " P & x in Q )
[#] Y <> {} ;
hence Q is open by A5, A11, TOPS_2:43; :: thesis: ( Q c= g " P & x in Q )
thus Q c= g " P :: thesis: x in Q

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Q or a in g " P )
assume A16: a in Q ; :: thesis: a in g " P
then g . a in rng g by A3, FUNCT_1:def 3;
then consider ga being Function such that
A17: g . a = ga and
A18: dom ga = M and
A19: rng ga c= the carrier of Y by A3, FUNCT_2:def 2;
A20: fi . a in V by A16, FUNCT_2:38;

now :: thesis: for z being object st z in M holds
ga . z in ((Carrier (M --> Y)) +* (i,V)) . z

let z be object ; :: thesis: ( z in M implies ga . z in ((Carrier (M --> Y)) +* (i,V)) . z )
assume A21: z in M ; :: thesis: ga . z in ((Carrier (M --> Y)) +* (i,V)) . z
then ( ( z <> i & (M --> the carrier of Y) . z = the carrier of Y ) or z = i ) by FUNCOP_1:7;
then ( ( z <> i & ga . z in rng ga & ((Carrier (M --> Y)) +* (i,V)) . z = the carrier of Y ) or z = i ) by A1, A18, A21, FUNCT_1:def 3, FUNCT_7:32;
hence ga . z in ((Carrier (M --> Y)) +* (i,V)) . z by A2, A10, A16, A20, A17, A19, FUNCT_6:56; :: thesis: verum

end;

then ga in P by A7, A8, A9, A18, CARD_3:9;
hence a in g " P by A16, A17, FUNCT_2:38; :: thesis: verum

end;

gx . i in V by A8, A9, A10, A14;
hence x in Q by A12, A15, FUNCT_2:38; :: 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:25; :: thesis: verum

end;

hence commute f is continuous Function of X,(M -TOP_prod (M --> Y)) by YELLOW_9:36; :: thesis: verum