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