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 object ; :: 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 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 ;
reconsider g = g as continuous Function of X,Y by ;
h = f * g by ;
then A6: a = f . (g . x) by ;
g . x in pi (A,x) by ;
hence a in f .: (pi (A,x)) by ; :: thesis: verum
end;
let a be object ; :: 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 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 ;
reconsider g = g as continuous Function of X,Y by ;
f * g = (oContMaps (X,f)) . g by Def2;
then A11: f * g in (oContMaps (X,f)) .: A by ;
a = (f * g) . x by ;
hence a in pi (((oContMaps (X,f)) .: A),x) by ; :: thesis: verum