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

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