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 5();
rng F c= the carrier of (oContMaps (Y,X))

proof

let y be object ; :: 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 object such that
A11: x in dom F and
A12: y = F . x by FUNCT_1:def 3;
reconsider g = x as continuous Function of Z,X by A9, A11, Th2;
y = f (#) g by A9, A10, A11, A12
.= g * f ;
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:2;
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 ;
:: thesis: verum