for k being object st k in dom (0 (#) f) holds
(0 (#) f) . k is empty by ORDINAL1:def 13;
hence 0 (#) f is empty-yielding by FUNCT_1:def 8; :: thesis: verum