let X be non empty TopSpace; :: thesis: for D being non empty a_partition of the carrier of X holds rng (Proj D) = the carrier of (space D)
let D be non empty a_partition of the carrier of X; :: thesis: rng (Proj D) = the carrier of (space D)
thus rng (Proj D) c= the carrier of (space D) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (space D) c= rng (Proj D)
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the carrier of (space D) or e in rng (Proj D) )
assume e in the carrier of (space D) ; :: thesis: e in rng (Proj D)
then ex p being Point of X st (Proj D) . p = e by Th29;
hence e in rng (Proj D) by FUNCT_2:4; :: thesis: verum