deffunc H1( Function) -> set = commute $1;
consider F being Function such that
A3:
dom F = the carrier of (oContMaps (X,(M -TOP_prod (M => Y))))
and
A4:
for f being Element of (oContMaps (X,(M -TOP_prod (M => Y)))) holds F . f = H1(f)
from FUNCT_1:sch 4();
rng F c= the carrier of ((oContMaps (X,Y)) |^ M)
proof
let y be
object ;
TARSKI:def 3 ( not y in rng F or y in the carrier of ((oContMaps (X,Y)) |^ M) )
assume
y in rng F
;
y in the carrier of ((oContMaps (X,Y)) |^ M)
then consider x being
object such that A5:
x in dom F
and A6:
y = F . x
by FUNCT_1:def 3;
reconsider x =
x as
Element of
(oContMaps (X,(M -TOP_prod (M => Y)))) by A3, A5;
reconsider f =
x as
continuous Function of
X,
(M -TOP_prod (M => Y)) by WAYBEL26:2;
(
commute f is
Function of
M, the
carrier of
(oContMaps (X,Y)) &
y = commute x )
by A4, A6, WAYBEL26:31;
then
y in Funcs (
M, the
carrier of
(oContMaps (X,Y)))
by FUNCT_2:8;
hence
y in the
carrier of
((oContMaps (X,Y)) |^ M)
by YELLOW_1:28;
verum
end;
then reconsider F = F as Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) by A3, FUNCT_2:2;
take
F
; for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F . f = commute f
let f be continuous Function of X,(M -TOP_prod (M => Y)); F . f = commute f
f is Element of (oContMaps (X,(M -TOP_prod (M => Y))))
by WAYBEL26:2;
hence
F . f = commute f
by A4; verum