let A, B, C be non empty RelStr ; :: thesis: for f, g being Function st f in MonFuncs (A,B) & g in MonFuncs (B,C) holds
g * f in MonFuncs (A,C)
let f, g be Function; :: thesis: ( f in MonFuncs (A,B) & g in MonFuncs (B,C) implies g * f in MonFuncs (A,C) )
assume that
A1: f in MonFuncs (A,B) and
A2: g in MonFuncs (B,C) ; :: thesis: g * f in MonFuncs (A,C)
consider f9 being Function of A,B such that
A3: f = f9 and
f9 in Funcs ( the carrier of A, the carrier of B) and
A4: f9 is monotone by A1, Def6;
consider g9 being Function of B,C such that
A5: g = g9 and
g9 in Funcs ( the carrier of B, the carrier of C) and
A6: g9 is monotone by A2, Def6;
consider gf being Function of A,C such that
A7: ( gf = g9 * f9 & gf is monotone ) by A4, A6, Lm1;
gf in Funcs ( the carrier of A, the carrier of C) by FUNCT_2:8;
hence g * f in MonFuncs (A,C) by A3, A5, A7, Def6; :: thesis: verum