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 object ; :: 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:13;
the carrier of (M -TOP_prod (M --> Y)) = product (Carrier (M --> Y)) by WAYBEL18:def 3
.= product (M --> the carrier of Y) by Th30 ;
then consider h being Function such that
A4: g = h and
A5: dom h = M and
A6: for x being object 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 object ; :: 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 object such that
A7: x in dom h and
A8: y = h . x by FUNCT_1:def 3;
(M --> the carrier of Y) . x = the carrier of Y by A5, A7, FUNCOP_1:7;
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:55;
A10: rng (commute f) c= the carrier of (oContMaps (X,Y))

proof

let g be object ; :: 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 object such that
A11: i in dom (commute f) and
A12: g = (commute f) . i by FUNCT_1:def 3;
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:7;
g = (proj ((M --> Y),i)) * f by A12, Th29;
then g is continuous Function of X,Y by A13, WAYBEL18:6;
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:2; :: thesis: verum