let L1, L2, L3 be non empty RelStr ; :: thesis: for f being Function of L1,L2
for g being Function of L2,L3 st f is monotone & g is monotone holds
g * f is monotone
let g1 be Function of L1,L2; :: thesis: for g being Function of L2,L3 st g1 is monotone & g is monotone holds
g * g1 is monotone
let g2 be Function of L2,L3; :: thesis: ( g1 is monotone & g2 is monotone implies g2 * g1 is monotone )
assume that
A1: g1 is monotone and
A2: g2 is monotone ; :: thesis: g2 * g1 is monotone
let s1, s2 be Element of L1; :: according to ORDERS_3:def 5 :: thesis: ( not s1 <= s2 or for b₁, b₂ being Element of the carrier of L3 holds
( not b₁ = (g2 * g1) . s1 or not b₂ = (g2 * g1) . s2 or b₁ <= b₂ ) )
assume s1 <= s2 ; :: thesis: for b₁, b₂ being Element of the carrier of L3 holds
( not b₁ = (g2 * g1) . s1 or not b₂ = (g2 * g1) . s2 or b₁ <= b₂ )
then g1 . s1 <= g1 . s2 by A1;
then g2 . (g1 . s1) <= g2 . (g1 . s2) by A2;
then (g2 * g1) . s1 <= g2 . (g1 . s2) by FUNCT_2:15;
hence for b₁, b₂ being Element of the carrier of L3 holds
( not b₁ = (g2 * g1) . s1 or not b₂ = (g2 * g1) . s2 or b₁ <= b₂ ) by FUNCT_2:15; :: thesis: verum