let X, Y, Z be non empty TopSpace; :: thesis: for f being continuous Function of Y,Z holds oContMaps f,X is monotone
let f be continuous Function of Y,Z; :: thesis: oContMaps f,X is monotone
( 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 f' = f as continuous Function of (Omega Y),(Omega Z) by YELLOW12:36;
set Xf = oContMaps f,X;
let a, b be Element of (oContMaps Z,X); :: according to WAYBEL_1:def 2 :: thesis: ( not a <= b or (oContMaps f,X) . a <= (oContMaps f,X) . b )
reconsider g1 = a, g2 = b as continuous Function of Z,(Omega X) by Th1;
assume a <= b ; :: thesis: (oContMaps f,X) . a <= (oContMaps f,X) . b
then A1: g1 <= g2 by Th3;
( g1 is continuous Function of Z,X & g2 is continuous Function of Z,X ) by Th2;
then A2: ( (oContMaps f,X) . a = g1 * f' & (oContMaps f,X) . b = g2 * f' ) by Def3;
then reconsider fg1 = g1 * f', fg2 = g2 * f' as Function of Y,(Omega X) by Th1;

now

let x be set ; :: thesis: ( x in the carrier of Y implies ex a, b being Element of (Omega X) st
( a = (g1 * f) . x & b = (g2 * f) . x & a <= b ) )
assume x in the carrier of Y ; :: thesis: ex a, b being Element of (Omega X) st
( a = (g1 * f) . x & b = (g2 * f) . x & a <= b )
then reconsider x' = x as Element of Y ;
( (g1 * f) . x' = g1 . (f . x') & (g2 * f) . x' = g2 . (f . x') ) by FUNCT_2:21;
hence ex a, b being Element of (Omega X) st
( a = (g1 * f) . x & b = (g2 * f) . x & a <= b ) by A1, YELLOW_2:def 1; :: thesis: verum

end;

then fg1 <= fg2 by YELLOW_2:def 1;
hence (oContMaps f,X) . a <= (oContMaps f,X) . b by A2, Th3; :: thesis: verum