not [:{[f,x]},(f . x):] is empty ;
then not rng (renameElementsDistinctlyFunc (f,x)) is empty by Th80;
hence not renameElementsDistinctlyFunc (f,x) is empty ; :: thesis: verum