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 = x2let 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 A2:
(
x1 in the
carrier of
(oContMaps X,(M -TOP_prod (M => Y))) &
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 )then reconsider a1 =
x1,
a2 =
x2 as
Element of
(oContMaps X,(M -TOP_prod (M => Y))) ;
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 = x2then 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, A2, 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 A3:
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) c= Funcs the
carrier of
X,the
carrier of
Y & the
carrier of
((oContMaps X,Y) |^ M) = Funcs M,the
carrier of
(oContMaps X,Y) )
by WAYBEL26:33, YELLOW_1:28;
then A5:
the
carrier of
((oContMaps X,Y) |^ M) c= Funcs M,
(Funcs the carrier of X,the carrier of Y)
by FUNCT_5:63;
reconsider x =
x as
Function of
M,the
carrier of
(oContMaps X,Y) by A4, 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;
commute (commute x) = x
by A3, A5, FUNCT_6:87;
then
(
(commute X,M,Y) . y = x &
dom (commute X,M,Y) = the
carrier of
(oContMaps X,(M -TOP_prod (M => Y))) )
by Def5, FUNCT_2:def 1;
hence
x in rng (commute X,M,Y)
by FUNCT_1:def 5;
:: thesis: verum
end;
hence
commute X,M,Y is onto
by FUNCT_2:def 3; :: thesis: verum