let A, B, C be non empty RelStr ; :: thesis: for f being Function of B,C
for g, h being Function of A,B st g <= h & f is monotone holds
f * g <= f * h
let f be Function of B,C; :: thesis: for g, h being Function of A,B st g <= h & f is monotone holds
f * g <= f * h
let g, h be Function of A,B; :: thesis: ( g <= h & f is monotone implies f * g <= f * h )
assume that
A1: g <= h and
A2: for x, y being Element of B st x <= y holds
f . x <= f . y ; :: according to WAYBEL_1:def 2 :: thesis: f * g <= f * h
for x being Element of A holds (f * g) . x <= (f * h) . x

proof

let x be Element of A; :: thesis: (f * g) . x <= (f * h) . x
A3: ( (f * g) . x = f . (g . x) & (f * h) . x = f . (h . x) ) by FUNCT_2:15;
g . x <= h . x by A1, YELLOW_2:9;
hence (f * g) . x <= (f * h) . x by A2, A3; :: thesis: verum

end;

hence f * g <= f * h by YELLOW_2:9; :: thesis: verum