deffunc H₁( 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 = H₁(f) from FUNCT_1:sch 4();
rng F c= the carrier of ((oContMaps (X,Y)) |^ M)

proof

let y be object ; :: 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 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; :: 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:2;
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