let x be set ; :: according to VALUED_0:def 9 :: thesis: ( not x in proj1 (f |^ a) or not (f |^ a) . x is V34() )
set g = f |^ a;
assume x in dom (f |^ a) ; :: thesis: (f |^ a) . x is V34()
then (f |^ a) . x = (f . x) |^ a by Def1;
hence (f |^ a) . x is V34() ; :: thesis: verum