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