consider f being Function such that
A1: ( dom f = X & rng f = {0} ) by FUNCT_1:5;
reconsider f = f as X -defined total Function by A1, PARTFUN1:def 2, RELAT_1:def 18;
f is empty-yielding by A1, RELAT_1:def 15;
hence ex b₁ being empty-yielding X -defined Function st b₁ is total ; :: thesis: verum