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