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

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

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

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

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

proof

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

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