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

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