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