let X, Y be non empty TopSpace; :: thesis: for M being non empty set
for f being continuous Function of X,(M -TOP_prod (M --> Y)) holds commute f is Function of M,the carrier of (oContMaps X,Y)
let M be non empty set ; :: thesis: for f being continuous Function of X,(M -TOP_prod (M --> Y)) holds commute f is Function of M,the carrier of (oContMaps X,Y)
let f be continuous Function of X,(M -TOP_prod (M --> Y)); :: thesis: commute f is Function of M,the carrier of (oContMaps X,Y)
A1: rng f c= Funcs M,the carrier of Y

proof

let g be set ; :: according to TARSKI:def 3 :: thesis: ( not g in rng f or g in Funcs M,the carrier of Y )
assume A2: g in rng f ; :: thesis: g in Funcs M,the carrier of Y
A3: dom (M --> the carrier of Y) = M by FUNCOP_1:19;
the carrier of (M -TOP_prod (M --> Y)) = product (Carrier (M --> Y)) by WAYBEL18:def 3
.= product (M --> the carrier of Y) by Th31 ;
then consider h being Function such that
A4: g = h and
A5: dom h = M and
A6: for x being set st x in M holds
h . x in (M --> the carrier of Y) . x by A2, A3, CARD_3:def 5;
rng h c= the carrier of Y

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng h or y in the carrier of Y )
assume y in rng h ; :: thesis: y in the carrier of Y
then consider x being set such that
A7: x in dom h and
A8: y = h . x by FUNCT_1:def 5;
(M --> the carrier of Y) . x = the carrier of Y by A5, A7, FUNCOP_1:13;
hence y in the carrier of Y by A5, A6, A7, A8; :: thesis: verum

end;

hence g in Funcs M,the carrier of Y by A4, A5, FUNCT_2:def 2; :: thesis: verum

end;

dom f = the carrier of X by FUNCT_2:def 1;
then f in Funcs the carrier of X,(Funcs M,the carrier of Y) by A1, FUNCT_2:def 2;
then A9: commute f in Funcs M,(Funcs the carrier of X,the carrier of Y) by FUNCT_6:85;
A10: rng (commute f) c= the carrier of (oContMaps X,Y)

proof

let g be set ; :: according to TARSKI:def 3 :: thesis: ( not g in rng (commute f) or g in the carrier of (oContMaps X,Y) )
assume g in rng (commute f) ; :: thesis: g in the carrier of (oContMaps X,Y)
then consider i being set such that
A11: i in dom (commute f) and
A12: g = (commute f) . i by FUNCT_1:def 5;
ex h being Function st
( commute f = h & dom h = M & rng h c= Funcs the carrier of X,the carrier of Y ) by A9, FUNCT_2:def 2;
then reconsider i = i as Element of M by A11;
A13: (M --> Y) . i = Y by FUNCOP_1:13;
g = (proj (M --> Y),i) * f by A12, Th30;
then g is continuous Function of X,Y by A13, WAYBEL18:7;
then g is Element of (oContMaps X,Y) by Th2;
hence g in the carrier of (oContMaps X,Y) ; :: thesis: verum

end;

ex g being Function st
( commute f = g & dom g = M & rng g c= Funcs the carrier of X,the carrier of Y ) by A9, FUNCT_2:def 2;
hence commute f is Function of M,the carrier of (oContMaps X,Y) by A10, FUNCT_2:4; :: thesis: verum