let X, Y, Z be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: pi ((oContMaps f,X) .: A),x = pi A,(f . x)
thus
pi ((oContMaps f,X) .: A),x c= pi A,(f . x)
:: according to XBOOLE_0:def 10 :: thesis: pi A,(f . x) c= pi ((oContMaps f,X) .: A),xproof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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
;
:: thesis: a in pi A,(f . x)
then consider h being
Function such that A1:
(
h in (oContMaps f,X) .: A &
a = h . x )
by CARD_3:def 6;
consider g being
set such that A2:
(
g in the
carrier of
(oContMaps Z,X) &
g in A &
h = (oContMaps f,X) . g )
by A1, FUNCT_2:115;
reconsider g =
g as
continuous Function of
Z,
X by A2, Th2;
h = g * f
by A2, Def3;
then
a = g . (f . x)
by A1, FUNCT_2:21;
hence
a in pi A,
(f . x)
by A2, CARD_3:def 6;
:: thesis: verum
end;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in pi A,(f . x) or a in pi ((oContMaps f,X) .: A),x )
assume
a in pi A,(f . x)
; :: thesis: a in pi ((oContMaps f,X) .: A),x
then consider g being Function such that
A3:
( g in A & a = g . (f . x) )
by CARD_3:def 6;
reconsider g = g as continuous Function of Z,X by A3, Th2;
A4:
a = (g * f) . x
by A3, FUNCT_2:21;
( g * f = (oContMaps f,X) . g & the carrier of (oContMaps Y,X) <> {} )
by Def3;
then
g * f in (oContMaps f,X) .: A
by A3, FUNCT_2:43;
hence
a in pi ((oContMaps f,X) .: A),x
by A4, CARD_3:def 6; :: thesis: verum