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),x)
proof
let a be object ; :: 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 and
A2: a = h . x by CARD_3:def 6;
consider g being object such that
A3: g in the carrier of (oContMaps (Z,X)) and
A4: g in A and
A5: h = (oContMaps (f,X)) . g by ;
reconsider g = g as continuous Function of Z,X by ;
h = g * f by ;
then a = g . (f . x) by ;
hence a in pi (A,(f . x)) by ; :: thesis: verum
end;
let a be object ; :: 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
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 ;
g * f = (oContMaps (f,X)) . g by Def3;
then A8: g * f in (oContMaps (f,X)) .: A by ;
a = (g * f) . x by ;
hence a in pi (((oContMaps (f,X)) .: A),x) by ; :: thesis: verum