let x be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in proj1 (i |-> 0) or (i |-> 0) . x is empty )
dom (i |-> 0) = Seg i by FUNCOP_1:13;
hence ( not x in proj1 (i |-> 0) or (i |-> 0) . x is empty ) by FINSEQ_2:57; :: thesis: verum