let e1 be ExtReal; :: according to VALUED_0:def 14 :: thesis: for e2 being ExtReal st e1 in dom (f * g) & e2 in dom (f * g) & e1 < e2 holds
(f * g) . e1 > (f * g) . e2
let e2 be ExtReal; :: thesis: ( e1 in dom (f * g) & e2 in dom (f * g) & e1 < e2 implies (f * g) . e1 > (f * g) . e2 )
assume that
A8: e1 in dom (f * g) and
A9: e2 in dom (f * g) ; :: thesis: ( not e1 < e2 or (f * g) . e1 > (f * g) . e2 )
A10: e1 in dom g by A8, FUNCT_1:11;
then A11: (f * g) . e1 = f . (g . e1) by FUNCT_1:13;
A12: e2 in dom g by A9, FUNCT_1:11;
then A13: (f * g) . e2 = f . (g . e2) by FUNCT_1:13;
assume e1 < e2 ; :: thesis: (f * g) . e1 > (f * g) . e2
then A14: g . e1 < g . e2 by A10, A12, Def9;
( g . e1 in dom f & g . e2 in dom f ) by A8, A9, FUNCT_1:11;
hence (f * g) . e1 > (f * g) . e2 by A11, A13, A14, Def10; :: thesis: verum