let X, Y, Z be non empty TopSpace; for f being continuous Function of Y,Z
for x being Element of X
for A being Subset of (oContMaps (X,Y)) holds pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))
let f be continuous Function of Y,Z; for x being Element of X
for A being Subset of (oContMaps (X,Y)) holds pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))
set Xf = oContMaps (X,f);
let x be Element of X; for A being Subset of (oContMaps (X,Y)) holds pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))
let A be Subset of (oContMaps (X,Y)); pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))
thus
pi (((oContMaps (X,f)) .: A),x) c= f .: (pi (A,x))
XBOOLE_0:def 10 f .: (pi (A,x)) c= pi (((oContMaps (X,f)) .: A),x)proof
let a be
object ;
TARSKI:def 3 ( not a in pi (((oContMaps (X,f)) .: A),x) or a in f .: (pi (A,x)) )
assume
a in pi (
((oContMaps (X,f)) .: A),
x)
;
a in f .: (pi (A,x))
then consider h being
Function such that A1:
h in (oContMaps (X,f)) .: A
and A2:
a = h . x
by CARD_3:def 6;
consider g being
object such that A3:
g in the
carrier of
(oContMaps (X,Y))
and A4:
g in A
and A5:
h = (oContMaps (X,f)) . g
by A1, FUNCT_2:64;
reconsider g =
g as
continuous Function of
X,
Y by A3, Th2;
h = f * g
by A5, Def2;
then A6:
a = f . (g . x)
by A2, FUNCT_2:15;
g . x in pi (
A,
x)
by A4, CARD_3:def 6;
hence
a in f .: (pi (A,x))
by A6, FUNCT_2:35;
verum
end;
let a be object ; TARSKI:def 3 ( not a in f .: (pi (A,x)) or a in pi (((oContMaps (X,f)) .: A),x) )
assume
a in f .: (pi (A,x))
; a in pi (((oContMaps (X,f)) .: A),x)
then consider b being object such that
b in the carrier of Y
and
A7:
b in pi (A,x)
and
A8:
a = f . b
by FUNCT_2:64;
consider g being Function such that
A9:
g in A
and
A10:
b = g . x
by A7, CARD_3:def 6;
reconsider g = g as continuous Function of X,Y by A9, Th2;
f * g = (oContMaps (X,f)) . g
by Def2;
then A11:
f * g in (oContMaps (X,f)) .: A
by A9, FUNCT_2:35;
a = (f * g) . x
by A8, A10, FUNCT_2:15;
hence
a in pi (((oContMaps (X,f)) .: A),x)
by A11, CARD_3:def 6; verum