let e1 be ext-real number ; :: according to VALUED_0:def 15 :: thesis: for e2 being ext-real number st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds
(g * f) . e1 <= (g * f) . e2
let e2 be ext-real number ; :: thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 <= (g * f) . e2 )
assume Z: ( e1 in dom (g * f) & e2 in dom (g * f) ) ; :: thesis: ( not e1 <= e2 or (g * f) . e1 <= (g * f) . e2 )
then A1: ( e1 in dom f & e2 in dom f ) by FUNCT_1:21;
then A4: ( (g * f) . e1 = g . (f . e1) & (g * f) . e2 = g . (f . e2) ) by FUNCT_1:23;
A3: ( f . e1 in dom g & f . e2 in dom g ) by Z, FUNCT_1:21;
assume e1 <= e2 ; :: thesis: (g * f) . e1 <= (g * f) . e2
then f . e1 <= f . e2 by A1, Def15;
hence (g * f) . e1 <= (g * f) . e2 by A3, A4, Def15; :: thesis: verum