let XX be non empty TopSpace; :: thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
let X be non empty SubSpace of XX; :: thesis: for D being non empty a_partition of the carrier of X
for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
let D be non empty a_partition of the carrier of X; :: thesis: for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W
let W be Point of XX; :: thesis: ( W in the carrier of X implies (Proj (TrivExt D)) . W = (Proj D) . W )
assume A1: W in the carrier of X ; :: thesis: (Proj (TrivExt D)) . W = (Proj D) . W
then reconsider p = W as Point of X ;
( D c= TrivExt D & (proj D) . p in D ) by XBOOLE_1:7;
then reconsider A = (Proj D) . W as Element of TrivExt D ;
W in A by A1, EQREL_1:def 9;
hence (Proj (TrivExt D)) . W = (Proj D) . W by EQREL_1:65; :: thesis: verum