deffunc H₁( 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₁(x) from FUNCT_1:sch 5();
rng F c= the carrier of (oContMaps (X,Z))

proof

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;

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