set f = v tohilbval ;
set D = dom (v tohilbval);
set C = rng (v tohilbval);
assume v tohilbval is V8() ; :: thesis: contradiction
then consider x being object such that
B0: ( x in dom (v tohilbval) & {} = (v tohilbval) . x ) by FUNCT_1:def 3;
reconsider n = x as Element of NAT by B0;
(v tohilbval) . n = dom ((v . n) tohilb) by Lm34;
hence contradiction by CARD_1:49, B0; :: thesis: verum