deffunc H1( 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 = H1(x)
from FUNCT_1:sch 5();
rng F c= the carrier of (oContMaps (X,Z))
proof
let y be
object ;
TARSKI:def 3 ( not y in rng F or y in the carrier of (oContMaps (X,Z)) )
assume
y in rng F
;
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))
;
verum
end;
then reconsider F = F as Function of (oContMaps (X,Y)),(oContMaps (X,Z)) by A3, FUNCT_2:2;
take
F
; for g being continuous Function of X,Y holds F . g = f * g
let g be continuous Function of X,Y; F . g = f * g
g is Element of (oContMaps (X,Y))
by Th2;
hence F . g =
g (#) f
by A4
.=
f * g
;
verum