not 0 in dom f by FINSEQ_3:24;
hence f . 0 = 0 by FUNCT_1:def 2; :: thesis: verum