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

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