let X be non empty TopSpace; :: thesis: for D being non empty a_partition of the carrier of X

for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W

let D be non empty a_partition of the carrier of X; :: thesis: for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W

let W be Point of (space D); :: thesis: ex W9 being Point of X st (Proj D) . W9 = W

reconsider p = W as Element of D by Def7;

consider W9 being Point of X such that

A1: (proj D) . W9 = p by EQREL_1:68;

take W9 ; :: thesis: (Proj D) . W9 = W

thus (Proj D) . W9 = W by A1; :: thesis: verum

for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W

let D be non empty a_partition of the carrier of X; :: thesis: for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W

let W be Point of (space D); :: thesis: ex W9 being Point of X st (Proj D) . W9 = W

reconsider p = W as Element of D by Def7;

consider W9 being Point of X such that

A1: (proj D) . W9 = p by EQREL_1:68;

take W9 ; :: thesis: (Proj D) . W9 = W

thus (Proj D) . W9 = W by A1; :: thesis: verum