let X, Y, Z be non empty TopSpace; :: thesis: for f being continuous Function of Y,Z holds oContMaps (X,f) is monotone

let f be continuous Function of Y,Z; :: thesis: oContMaps (X,f) is monotone

let a, b be Element of (oContMaps (X,Y)); :: according to WAYBEL_1:def 2 :: thesis: ( not a <= b or (oContMaps (X,f)) . a <= (oContMaps (X,f)) . b )

( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) & TopStruct(# the carrier of Z, the topology of Z #) = TopStruct(# the carrier of (Omega Z), the topology of (Omega Z) #) ) by WAYBEL25:def 2;

then reconsider f9 = f as continuous Function of (Omega Y),(Omega Z) by YELLOW12:36;

reconsider g1 = a, g2 = b as continuous Function of X,(Omega Y) by Th1;

set Xf = oContMaps (X,f);

reconsider fg1 = f9 * g1, fg2 = f9 * g2 as Function of X,(Omega Z) ;

g2 is continuous Function of X,Y by Th2;

then A1: (oContMaps (X,f)) . b = f9 * g2 by Def2;

assume a <= b ; :: thesis: (oContMaps (X,f)) . a <= (oContMaps (X,f)) . b

then A2: g1 <= g2 by Th3;

g1 is continuous Function of X,Y by Th2;

then (oContMaps (X,f)) . a = f9 * g1 by Def2;

hence (oContMaps (X,f)) . a <= (oContMaps (X,f)) . b by A1, A4, Th3; :: thesis: verum

let f be continuous Function of Y,Z; :: thesis: oContMaps (X,f) is monotone

let a, b be Element of (oContMaps (X,Y)); :: according to WAYBEL_1:def 2 :: thesis: ( not a <= b or (oContMaps (X,f)) . a <= (oContMaps (X,f)) . b )

( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) & TopStruct(# the carrier of Z, the topology of Z #) = TopStruct(# the carrier of (Omega Z), the topology of (Omega Z) #) ) by WAYBEL25:def 2;

then reconsider f9 = f as continuous Function of (Omega Y),(Omega Z) by YELLOW12:36;

reconsider g1 = a, g2 = b as continuous Function of X,(Omega Y) by Th1;

set Xf = oContMaps (X,f);

reconsider fg1 = f9 * g1, fg2 = f9 * g2 as Function of X,(Omega Z) ;

g2 is continuous Function of X,Y by Th2;

then A1: (oContMaps (X,f)) . b = f9 * g2 by Def2;

assume a <= b ; :: thesis: (oContMaps (X,f)) . a <= (oContMaps (X,f)) . b

then A2: g1 <= g2 by Th3;

now :: thesis: for x being set st x in the carrier of X holds

ex a, b being Element of (Omega Z) st

( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b )

then A4:
fg1 <= fg2
;ex a, b being Element of (Omega Z) st

( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b )

let x be set ; :: thesis: ( x in the carrier of X implies ex a, b being Element of (Omega Z) st

( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b ) )

assume x in the carrier of X ; :: thesis: ex a, b being Element of (Omega Z) st

( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b )

then reconsider x9 = x as Element of X ;

A3: (f9 * g2) . x9 = f9 . (g2 . x9) by FUNCT_2:15;

( ex a, b being Element of (Omega Y) st

( a = g1 . x9 & b = g2 . x9 & a <= b ) & (f9 * g1) . x9 = f9 . (g1 . x9) ) by A2, FUNCT_2:15;

then (f9 * g1) . x9 <= (f9 * g2) . x9 by A3, WAYBEL_1:def 2;

hence ex a, b being Element of (Omega Z) st

( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b ) ; :: thesis: verum

end;( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b ) )

assume x in the carrier of X ; :: thesis: ex a, b being Element of (Omega Z) st

( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b )

then reconsider x9 = x as Element of X ;

A3: (f9 * g2) . x9 = f9 . (g2 . x9) by FUNCT_2:15;

( ex a, b being Element of (Omega Y) st

( a = g1 . x9 & b = g2 . x9 & a <= b ) & (f9 * g1) . x9 = f9 . (g1 . x9) ) by A2, FUNCT_2:15;

then (f9 * g1) . x9 <= (f9 * g2) . x9 by A3, WAYBEL_1:def 2;

hence ex a, b being Element of (Omega Z) st

( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b ) ; :: thesis: verum

g1 is continuous Function of X,Y by Th2;

then (oContMaps (X,f)) . a = f9 * g1 by Def2;

hence (oContMaps (X,f)) . a <= (oContMaps (X,f)) . b by A1, A4, Th3; :: thesis: verum