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

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