set F = r (#) f;
let a, b be ExtReal; :: according to VALUED_0:def 13 :: thesis: ( not a in proj1 (r (#) f) or not b in proj1 (r (#) f) or b <= a or not (r (#) f) . b <= (r (#) f) . a )
assume A1: ( a in dom (r (#) f) & b in dom (r (#) f) ) ; :: thesis: ( b <= a or not (r (#) f) . b <= (r (#) f) . a )
assume a < b ; :: thesis: not (r (#) f) . b <= (r (#) f) . a
then A2: f . a > f . b by A1, VALUED_0:def 14;
( (r (#) f) . a = r * (f . a) & (r (#) f) . b = r * (f . b) ) by VALUED_1:6;
hence not (r (#) f) . b <= (r (#) f) . a by A2, XREAL_1:69; :: thesis: verum