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 A1, FUNCT_2:64;
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:15;
hence a in pi (A,(f . x)) by A4, CARD_3:def 6; :: 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 A6, Th2;
g * f = (oContMaps (f,X)) . g by Def3;
then A8: g * f in (oContMaps (f,X)) .: A by A6, FUNCT_2:35;
a = (g * f) . x by A7, FUNCT_2:15;
hence a in pi (((oContMaps (f,X)) .: A),x) by A8, CARD_3:def 6; :: thesis: verum