deffunc H_{1}( 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_{1}(f)
from FUNCT_1:sch 4();

rng F c= the carrier of ((oContMaps (X,Y)) |^ M)

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

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

rng F c= the carrier of ((oContMaps (X,Y)) |^ M)

proof

then reconsider F = F as Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) by A3, FUNCT_2:2;
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;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

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