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)

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

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 (A,(f . x)) or a in pi (((oContMaps (f,X)) .: A),x) )
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;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

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