reconsider f = F _V as one-to-one Function ;
dom ((F ") _V) = rng f by FUNCT_1:33;
hence not F " is empty ; :: thesis: verum