set f = commute X,M,Y;
Carrier (M => Y) = M => the carrier of Y by WAYBEL26:31;
then the carrier of (M -TOP_prod (M => Y)) = product (M => the carrier of Y) by WAYBEL18:def 3
.= Funcs M,the carrier of Y by CARD_3:20 ;
then A1: the carrier of (oContMaps X,(M -TOP_prod (M => Y))) c= Funcs the carrier of X,(Funcs M,the carrier of Y) by WAYBEL26:33;

now

thus the carrier of ((oContMaps X,Y) |^ M) <> {} ; :: thesis: for x1, x2 being set st x1 in the carrier of (oContMaps X,(M -TOP_prod (M => Y))) & x2 in the carrier of (oContMaps X,(M -TOP_prod (M => Y))) & (commute X,M,Y) . x1 = (commute X,M,Y) . x2 holds
x1 = x2
let x1, x2 be set ; :: thesis: ( x1 in the carrier of (oContMaps X,(M -TOP_prod (M => Y))) & x2 in the carrier of (oContMaps X,(M -TOP_prod (M => Y))) & (commute X,M,Y) . x1 = (commute X,M,Y) . x2 implies x1 = x2 )
assume that
A2: x1 in the carrier of (oContMaps X,(M -TOP_prod (M => Y))) and
A3: x2 in the carrier of (oContMaps X,(M -TOP_prod (M => Y))) ; :: thesis: ( (commute X,M,Y) . x1 = (commute X,M,Y) . x2 implies x1 = x2 )
reconsider a1 = x1, a2 = x2 as Element of (oContMaps X,(M -TOP_prod (M => Y))) by A2, A3;
reconsider f1 = a1, f2 = a2 as continuous Function of X,(M -TOP_prod (M => Y)) by WAYBEL26:2;
assume (commute X,M,Y) . x1 = (commute X,M,Y) . x2 ; :: thesis: x1 = x2
then commute f1 = (commute X,M,Y) . x2 by Def5
.= commute f2 by Def5 ;
then f1 = commute (commute f2) by A1, A2, FUNCT_6:87;
hence x1 = x2 by A1, A3, FUNCT_6:87; :: thesis: verum

end;

hence commute X,M,Y is one-to-one by FUNCT_2:25; :: thesis: commute X,M,Y is onto
rng (commute X,M,Y) = the carrier of ((oContMaps X,Y) |^ M)

proof

thus rng (commute X,M,Y) c= the carrier of ((oContMaps X,Y) |^ M) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of ((oContMaps X,Y) |^ M) c= rng (commute X,M,Y)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of ((oContMaps X,Y) |^ M) or x in rng (commute X,M,Y) )
assume A4: x in the carrier of ((oContMaps X,Y) |^ M) ; :: thesis: x in rng (commute X,M,Y)
then reconsider x = x as Element of ((oContMaps X,Y) |^ M) ;
A5: the carrier of ((oContMaps X,Y) |^ M) = Funcs M,the carrier of (oContMaps X,Y) by YELLOW_1:28;
then reconsider x = x as Function of M,the carrier of (oContMaps X,Y) by FUNCT_2:121;
reconsider g = commute x as continuous Function of X,(M -TOP_prod (M => Y)) by WAYBEL26:34;
reconsider y = g as Element of (oContMaps X,(M -TOP_prod (M => Y))) by WAYBEL26:2;
the carrier of ((oContMaps X,Y) |^ M) c= Funcs M,(Funcs the carrier of X,the carrier of Y) by A5, FUNCT_5:63, WAYBEL26:33;
then commute (commute x) = x by A4, FUNCT_6:87;
then A6: (commute X,M,Y) . y = x by Def5;
dom (commute X,M,Y) = the carrier of (oContMaps X,(M -TOP_prod (M => Y))) by FUNCT_2:def 1;
hence x in rng (commute X,M,Y) by A6, FUNCT_1:def 5; :: thesis: verum

end;

hence commute X,M,Y is onto by FUNCT_2:def 3; :: thesis: verum