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
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in the carrier of ((oContMaps X,Y) |^ M) )
assume
y in rng F
;
:: thesis: y in the carrier of ((oContMaps X,Y) |^ M)
then consider x being
set such that A5:
(
x in dom F &
y = F . x )
by FUNCT_1:def 5;
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, A5, WAYBEL26:32;
then
y in Funcs M,the
carrier of
(oContMaps X,Y)
by FUNCT_2:11;
hence
y in the
carrier of
((oContMaps X,Y) |^ M)
by YELLOW_1:28;
:: thesis: verum
end;
then reconsider F = F as Function of (oContMaps X,(M -TOP_prod (M => Y))),((oContMaps X,Y) |^ M) by A3, FUNCT_2:4;
take
F
; :: thesis: 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)); :: thesis: 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; :: thesis: verum