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
( 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 X,f;
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 )
reconsider g1 = a, g2 = b as continuous Function of X,(Omega Y) by Th1;
assume a <= b ; :: thesis: (oContMaps X,f) . a <= (oContMaps X,f) . b
then A1: g1 <= g2 by Th3;
( g1 is continuous Function of X,Y & g2 is continuous Function of X,Y ) by Th2;
then A2: ( (oContMaps X,f) . a = f' * g1 & (oContMaps X,f) . b = f' * g2 ) by Def2;
reconsider fg1 = f' * g1, fg2 = f' * g2 as Function of X,(Omega Z) ;

now

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

end;

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