deffunc H₁( set ) -> set = f (#) $1;
consider F being Function such that
A9: dom F = the carrier of (oContMaps Z,X) and
A10: for x being set st x in the carrier of (oContMaps Z,X) holds
F . x = H₁(x) from FUNCT_1:sch 3();
rng F c= the carrier of (oContMaps Y,X)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in the carrier of (oContMaps Y,X) )
assume y in rng F ; :: thesis: y in the carrier of (oContMaps Y,X)
then consider x being set such that
A11: x in dom F and
A12: y = F . x by FUNCT_1:def 5;
reconsider g = x as continuous Function of Z,X by A9, A11, Th2;
y = f (#) g by A9, A10, A11, A12
.= g * f by YELLOW16:1 ;
then y is Element of (oContMaps Y,X) by Th2;
hence y in the carrier of (oContMaps Y,X) ; :: thesis: verum

end;

then reconsider F = F as Function of (oContMaps Z,X),(oContMaps Y,X) by A9, FUNCT_2:4;
take F ; :: thesis: for g being continuous Function of Z,X holds F . g = g * f
let g be continuous Function of Z,X; :: thesis: F . g = g * f
g is Element of (oContMaps Z,X) by Th2;
hence F . g = f (#) g by A10
.= g * f by YELLOW16:1 ;
:: thesis: verum