consider x being object such that
A1: x is_a_fixpoint_of f by ABIAN:def 5;
thus not dom f is empty by A1, ABIAN:def 3; :: thesis: verum