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, Lm2;
gf in Funcs the carrier of A,the carrier of C by FUNCT_2:11;
hence g * f in MonFuncs A,C by A3, A5, A7, Def6; :: thesis: verum