deffunc H_{1}( set ) -> set = $1 (#) f;

consider F being Function such that

A3: dom F = the carrier of (oContMaps (X,Y)) and

A4: for x being set st x in the carrier of (oContMaps (X,Y)) holds

F . x = H_{1}(x)
from FUNCT_1:sch 5();

rng F c= the carrier of (oContMaps (X,Z))

take F ; :: thesis: for g being continuous Function of X,Y holds F . g = f * g

let g be continuous Function of X,Y; :: thesis: F . g = f * g

g is Element of (oContMaps (X,Y)) by Th2;

hence F . g = g (#) f by A4

.= f * g ;

:: thesis: verum

consider F being Function such that

A3: dom F = the carrier of (oContMaps (X,Y)) and

A4: for x being set st x in the carrier of (oContMaps (X,Y)) holds

F . x = H

rng F c= the carrier of (oContMaps (X,Z))

proof

then reconsider F = F as Function of (oContMaps (X,Y)),(oContMaps (X,Z)) 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,Z)) )

assume y in rng F ; :: thesis: y in the carrier of (oContMaps (X,Z))

then consider x being object such that

A5: x in dom F and

A6: y = F . x by FUNCT_1:def 3;

reconsider g = x as continuous Function of X,Y by A3, A5, Th2;

y = g (#) f by A3, A4, A5, A6

.= f * g ;

then y is Element of (oContMaps (X,Z)) by Th2;

hence y in the carrier of (oContMaps (X,Z)) ; :: thesis: verum

end;assume y in rng F ; :: thesis: y in the carrier of (oContMaps (X,Z))

then consider x being object such that

A5: x in dom F and

A6: y = F . x by FUNCT_1:def 3;

reconsider g = x as continuous Function of X,Y by A3, A5, Th2;

y = g (#) f by A3, A4, A5, A6

.= f * g ;

then y is Element of (oContMaps (X,Z)) by Th2;

hence y in the carrier of (oContMaps (X,Z)) ; :: thesis: verum

take F ; :: thesis: for g being continuous Function of X,Y holds F . g = f * g

let g be continuous Function of X,Y; :: thesis: F . g = f * g

g is Element of (oContMaps (X,Y)) by Th2;

hence F . g = g (#) f by A4

.= f * g ;

:: thesis: verum