let A, B, C be non empty RelStr ; 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; 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; ( 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
; WAYBEL_1:def 2 f * g <= f * h
for x being Element of A holds (f * g) . x <= (f * h) . x
hence
f * g <= f * h
by YELLOW_2:9; verum