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