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