let X, Y, Z be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: pi ((oContMaps X,f) .: A),x = f .: (pi A,x)
thus pi ((oContMaps X,f) .: A),x c= f .: (pi A,x) :: according to XBOOLE_0:def 10 :: thesis: f .: (pi A,x) c= pi ((oContMaps X,f) .: A),x

proof

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

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in f .: (pi A,x) or a in pi ((oContMaps X,f) .: A),x )
assume a in f .: (pi A,x) ; :: thesis: a in pi ((oContMaps X,f) .: A),x
then consider b being set such that
A3: ( b in the carrier of Y & b in pi A,x & a = f . b ) by FUNCT_2:115;
consider g being Function such that
A4: ( g in A & b = g . x ) by A3, CARD_3:def 6;
reconsider g = g as continuous Function of X,Y by A4, Th2;
A5: a = (f * g) . x by A3, A4, FUNCT_2:21;
( f * g = (oContMaps X,f) . g & the carrier of (oContMaps X,Z) <> {} ) by Def2;
then f * g in (oContMaps X,f) .: A by A4, FUNCT_2:43;
hence a in pi ((oContMaps X,f) .: A),x by A5, CARD_3:def 6; :: thesis: verum