let A, B, C be non empty RelStr ; :: thesis: for f being Function of A,B

for g being Function of B,C st f is monotone & g is monotone holds

ex gf being Function of A,C st

( gf = g * f & gf is monotone )

let f be Function of A,B; :: thesis: for g being Function of B,C st f is monotone & g is monotone holds

ex gf being Function of A,C st

( gf = g * f & gf is monotone )

let g be Function of B,C; :: thesis: ( f is monotone & g is monotone implies ex gf being Function of A,C st

( gf = g * f & gf is monotone ) )

assume that

A1: f is monotone and

A2: g is monotone ; :: thesis: ex gf being Function of A,C st

( gf = g * f & gf is monotone )

reconsider gf = g * f as Function of A,C ;

take gf ; :: thesis: ( gf = g * f & gf is monotone )

for g being Function of B,C st f is monotone & g is monotone holds

ex gf being Function of A,C st

( gf = g * f & gf is monotone )

let f be Function of A,B; :: thesis: for g being Function of B,C st f is monotone & g is monotone holds

ex gf being Function of A,C st

( gf = g * f & gf is monotone )

let g be Function of B,C; :: thesis: ( f is monotone & g is monotone implies ex gf being Function of A,C st

( gf = g * f & gf is monotone ) )

assume that

A1: f is monotone and

A2: g is monotone ; :: thesis: ex gf being Function of A,C st

( gf = g * f & gf is monotone )

reconsider gf = g * f as Function of A,C ;

take gf ; :: thesis: ( gf = g * f & gf is monotone )

now :: thesis: for p1, p2 being Element of A st p1 <= p2 holds

for r1, r2 being Element of C st r1 = gf . p1 & r2 = gf . p2 holds

r1 <= r2

hence
( gf = g * f & gf is monotone )
; :: thesis: verumfor r1, r2 being Element of C st r1 = gf . p1 & r2 = gf . p2 holds

r1 <= r2

let p1, p2 be Element of A; :: thesis: ( p1 <= p2 implies for r1, r2 being Element of C st r1 = gf . p1 & r2 = gf . p2 holds

r1 <= r2 )

reconsider p19 = f . p1, p29 = f . p2 as Element of B ;

dom f = the carrier of A by FUNCT_2:def 1;

then A3: ( g . (f . p1) = (g * f) . p1 & g . (f . p2) = (g * f) . p2 ) by FUNCT_1:13;

assume p1 <= p2 ; :: thesis: for r1, r2 being Element of C st r1 = gf . p1 & r2 = gf . p2 holds

r1 <= r2

then A4: p19 <= p29 by A1;

let r1, r2 be Element of C; :: thesis: ( r1 = gf . p1 & r2 = gf . p2 implies r1 <= r2 )

assume ( r1 = gf . p1 & r2 = gf . p2 ) ; :: thesis: r1 <= r2

hence r1 <= r2 by A2, A3, A4; :: thesis: verum

end;r1 <= r2 )

reconsider p19 = f . p1, p29 = f . p2 as Element of B ;

dom f = the carrier of A by FUNCT_2:def 1;

then A3: ( g . (f . p1) = (g * f) . p1 & g . (f . p2) = (g * f) . p2 ) by FUNCT_1:13;

assume p1 <= p2 ; :: thesis: for r1, r2 being Element of C st r1 = gf . p1 & r2 = gf . p2 holds

r1 <= r2

then A4: p19 <= p29 by A1;

let r1, r2 be Element of C; :: thesis: ( r1 = gf . p1 & r2 = gf . p2 implies r1 <= r2 )

assume ( r1 = gf . p1 & r2 = gf . p2 ) ; :: thesis: r1 <= r2

hence r1 <= r2 by A2, A3, A4; :: thesis: verum