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),xproof
let a be
set ;
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
set 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:115;
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:21;
g . x in pi A,
x
by A4, CARD_3:def 6;
hence
a in f .: (pi A,x)
by A6, FUNCT_2:43;
verum
end;
let a be set ; 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 set such that
b in the carrier of Y
and
A7:
b in pi A,x
and
A8:
a = f . b
by FUNCT_2:115;
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:43;
a = (f * g) . x
by A8, A10, FUNCT_2:21;
hence
a in pi ((oContMaps X,f) .: A),x
by A11, CARD_3:def 6; verum