let x be object ; :: according to VALUED_0:def 9 :: thesis: ( not x in dom (r (#) f) or not (r (#) f) . x is V25() )
assume x in dom (r (#) f) ; :: thesis: (r (#) f) . x is V25()
then (r (#) f) . x = r * (f . x) by Def5;
hence (r (#) f) . x is V25() ; :: thesis: verum