set F = r (#) f;
let a, b be ExtReal; :: according to VALUED_0:def 16 :: thesis: ( not a in proj1 (r (#) f) or not b in proj1 (r (#) f) or not a <= b or (r (#) f) . b <= (r (#) f) . a )
assume A1: ( a in dom (r (#) f) & b in dom (r (#) f) ) ; :: thesis: ( not a <= b or (r (#) f) . b <= (r (#) f) . a )
assume a <= b ; :: thesis: (r (#) f) . b <= (r (#) f) . a
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) . b <= (r (#) f) . a by A2, XREAL_1:65; :: thesis: verum