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 A1: ( f in MonFuncs A,B & g in MonFuncs B,C ) ; :: thesis: g * f in MonFuncs A,C
then consider f' being Function of A,B such that
A2: ( f = f' & f' in Funcs the carrier of A,the carrier of B & f' is monotone ) by Def6;
consider g' being Function of B,C such that
A3: ( g = g' & g' in Funcs the carrier of B,the carrier of C & g' is monotone ) by A1, Def6;
consider gf being Function of A,C such that
A4: ( gf = g' * f' & gf is monotone ) by A2, A3, Lm3;
gf in Funcs the carrier of A,the carrier of C by FUNCT_2:11;
hence g * f in MonFuncs A,C by A2, A3, A4, Def6; :: thesis: verum