dom A = T by FUNCT_2:def 1;
hence ( A is empty-yielding iff for a being object st a in T holds
A . a = 0 ) by Lemma1; :: thesis: verum