let x be object ; :: according to PBOOLE:def 13 :: thesis: ( not x in I or not (rngs f) . x is empty )
assume A1: x in I ; :: thesis: not (rngs f) . x is empty
( (rngs f) . x = rng (f . x) & dom (f . x) = A . x ) by A1, FUNCT_2:def 1, MSSUBFAM:13;
hence not (rngs f) . x is empty by A1, RELAT_1:42; :: thesis: verum