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