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

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 ;
A3: (f' * g2) . x' = f' . (g2 . x') by FUNCT_2:21;
( ex a, b being Element of (Omega Y) st
( a = g1 . x' & b = g2 . x' & a <= b ) & (f' * g1) . x' = f' . (g1 . x') ) by A2, FUNCT_2:21, YELLOW_2:def 1;
then (f' * g1) . x' <= (f' * g2) . x' by A3, 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 A4: fg1 <= fg2 by YELLOW_2:def 1;
g1 is continuous Function of X,Y by Th2;
then (oContMaps X,f) . a = f' * g1 by Def2;
hence (oContMaps X,f) . a <= (oContMaps X,f) . b by A1, A4, Th3; :: thesis: verum