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