let x be object ; :: according to FUNCT_1:def 8 :: thesis: ( not x in dom (i |-> 0) or (i |-> 0) . x is empty )
thus ( not x in dom (i |-> 0) or (i |-> 0) . x is empty ) ; :: thesis: verum