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