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 A1:
( f is monotone & 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 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 )A2:
dom f = the
carrier of
A
by FUNCT_2:def 1;
assume A3:
p1 <= p2
;
:: thesis: for r1, r2 being Element of C st r1 = gf . p1 & r2 = gf . p2 holds
r1 <= r2reconsider p1' =
f . p1,
p2' =
f . p2 as
Element of
B ;
A4:
(
g . (f . p1) = (g * f) . p1 &
g . (f . p2) = (g * f) . p2 )
by A2, FUNCT_1:23;
A5:
p1' <= p2'
by A1, A3, Def5;
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 <= r2hence
r1 <= r2
by A1, A4, A5, Def5;
:: thesis: verum end;
hence
( gf = g * f & gf is monotone )
by Def5; :: thesis: verum