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