set f = commute (X,M,Y);
Carrier (M => Y) = M => the carrier of Y by WAYBEL26:30;
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:11 ;
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:32;

now :: thesis: ( the carrier of ((oContMaps (X,Y)) |^ M) <> {} & ( for x1, x2 being object 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 ) )

thus the carrier of ((oContMaps (X,Y)) |^ M) <> {} ; :: thesis: for x1, x2 being object 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 object ; :: 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, FUNCT_6:57;
hence x1 = x2 by A1, FUNCT_6:57; :: thesis: verum

end;

hence commute (X,M,Y) is one-to-one ; :: 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 object ; :: 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 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) ;
A4: 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:66;
reconsider g = commute x as continuous Function of X,(M -TOP_prod (M => Y)) by WAYBEL26:33;
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 A4, FUNCT_5:56, WAYBEL26:32;
then commute (commute x) = x by FUNCT_6:57;
then A5: (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 A5, FUNCT_1:def 3; :: thesis: verum

end;

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