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 )

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

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;

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