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: ( dom f = the carrier of X & rng f c= the carrier of (M -TOP_prod (M --> Y)) ) by FUNCT_2:def 1;
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
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 ( g in product (M --> the carrier of Y) & dom (M --> the carrier of Y) = M ) by A2, FUNCOP_1:19;
then consider h being Function such that
A3: ( g = h & dom h = M & ( for x being set st x in M holds
h . x in (M --> the carrier of Y) . x ) ) by 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
A4: ( x in dom h & y = h . x ) by FUNCT_1:def 5;
(M --> the carrier of Y) . x = the carrier of Y by A3, A4, FUNCOP_1:13;
hence y in the carrier of Y by A3, A4; :: thesis: verum

end;

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

end;

then f in Funcs the carrier of X,(Funcs M,the carrier of Y) by A1, FUNCT_2:def 2;
then A5: commute f in Funcs M,(Funcs the carrier of X,the carrier of Y) by FUNCT_6:85;
then A6: ex g being Function st
( commute f = g & dom g = M & rng g c= Funcs the carrier of X,the carrier of Y ) by FUNCT_2:def 2;
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
A7: ( i in dom (commute f) & 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 A5, FUNCT_2:def 2;
then reconsider i = i as Element of M by A7;
( g = (proj (M --> Y),i) * f & (M --> Y) . i = Y ) by A7, Th30, FUNCOP_1:13;
then g is continuous Function of X,Y by WAYBEL18:7;
then g is Element of (oContMaps X,Y) by Th2;
hence g in the carrier of (oContMaps X,Y) ; :: thesis: verum

end;

hence commute f is Function of M,the carrier of (oContMaps X,Y) by A6, FUNCT_2:4; :: thesis: verum