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