not {} in rng f ;
hence not product f is empty by Th37; :: thesis: verum