let f be Function; :: thesis: for W being Universe st dom f in W & rng f c= W holds
rng f in W
let W be Universe; :: thesis: ( dom f in W & rng f c= W implies rng f in W )
assume dom f in W ; :: thesis: ( not rng f c= W or rng f in W )
then ( rng f = f .: (dom f) & card (dom f) in card W ) by CLASSES2:1, RELAT_1:113;
then card (rng f) in card W by CARD_1:67, ORDINAL1:12;
hence ( not rng f c= W or rng f in W ) by CLASSES1:1; :: thesis: verum