let e1 be ExtReal; :: according to VALUED_0:def 15 :: thesis: for e2 being ExtReal st e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 holds
(g * f) . e1 <= (g * f) . e2
let e2 be ExtReal; :: thesis: ( e1 in dom (g * f) & e2 in dom (g * f) & e1 <= e2 implies (g * f) . e1 <= (g * f) . e2 )
assume that
A1: e1 in dom (g * f) and
A2: e2 in dom (g * f) ; :: thesis: ( not e1 <= e2 or (g * f) . e1 <= (g * f) . e2 )
A3: e1 in dom f by A1, FUNCT_1:11;
then A4: (g * f) . e1 = g . (f . e1) by FUNCT_1:13;
A5: e2 in dom f by A2, FUNCT_1:11;
then A6: (g * f) . e2 = g . (f . e2) by FUNCT_1:13;
assume e1 <= e2 ; :: thesis: (g * f) . e1 <= (g * f) . e2
then A7: f . e1 <= f . e2 by A3, A5, Def11;
( f . e1 in dom g & f . e2 in dom g ) by A1, A2, FUNCT_1:11;
hence (g * f) . e1 <= (g * f) . e2 by A4, A6, A7, Def11; :: thesis: verum