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 )
A1: rng f = f .: (dom f) by RELAT_1:146;
assume dom f in W ; :: thesis: ( not rng f c= W or rng f in W )
then ( card (dom f) in card W & card (rng f) c= card (dom f) ) by A1, CARD_2:3, CLASSES2:1;
then card (rng f) in card W by ORDINAL1:22;
hence ( not rng f c= W or rng f in W ) by CLASSES1:2; :: thesis: verum