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)

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 A7, CARD_3:def 6;

reconsider g = g as continuous Function of X,Y by A9, Th2;

f * g = (oContMaps (X,f)) . g by Def2;

then A11: f * g in (oContMaps (X,f)) .: A by A9, FUNCT_2:35;

a = (f * g) . x by A8, A10, FUNCT_2:15;

hence a in pi (((oContMaps (X,f)) .: A),x) by A11, CARD_3:def 6; :: thesis: verum

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

reconsider g = g as continuous Function of X,Y by A3, Th2;

h = f * g by A5, Def2;

then A6: a = f . (g . x) by A2, FUNCT_2:15;

g . x in pi (A,x) by A4, CARD_3:def 6;

hence a in f .: (pi (A,x)) by A6, FUNCT_2:35; :: thesis: verum

end;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 A1, FUNCT_2:64;

reconsider g = g as continuous Function of X,Y by A3, Th2;

h = f * g by A5, Def2;

then A6: a = f . (g . x) by A2, FUNCT_2:15;

g . x in pi (A,x) by A4, CARD_3:def 6;

hence a in f .: (pi (A,x)) by A6, FUNCT_2:35; :: thesis: verum

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 A7, CARD_3:def 6;

reconsider g = g as continuous Function of X,Y by A9, Th2;

f * g = (oContMaps (X,f)) . g by Def2;

then A11: f * g in (oContMaps (X,f)) .: A by A9, FUNCT_2:35;

a = (f * g) . x by A8, A10, FUNCT_2:15;

hence a in pi (((oContMaps (X,f)) .: A),x) by A11, CARD_3:def 6; :: thesis: verum