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;

rng (commute (X,M,Y)) = the carrier of ((oContMaps (X,Y)) |^ M)

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 ) )

hence
commute (X,M,Y) is V7()
; :: thesis: commute (X,M,Y) is onto 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;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

rng (commute (X,M,Y)) = the carrier of ((oContMaps (X,Y)) |^ M)

proof

hence
commute (X,M,Y) is onto
by FUNCT_2:def 3; :: thesis: verum
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;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