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 ( 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) <> {}
;
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 = x2let x1,
x2 be
object ;
( 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))))
;
( (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
;
x1 = x2then 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;
verum end;
hence
commute (X,M,Y) is V7()
; 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)
;
XBOOLE_0:def 10 the carrier of ((oContMaps (X,Y)) |^ M) c= rng (commute (X,M,Y))
let x be
object ;
TARSKI:def 3 ( 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)
;
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;
verum
end;
hence
commute (X,M,Y) is onto
by FUNCT_2:def 3; verum