reconsider X = dom f as set ;
dom (0 (#) f) = dom f by VALUED_1:def 5;
then reconsider h = 0 (#) f as empty-yielding X -defined Function by RELAT_1:def 18;
dom h = X by VALUED_1:def 5;
then h is total by PARTFUN1:def 2;
hence ex b₁ being empty-yielding dom f -defined Function st b₁ is total ; :: thesis: verum