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 )
A1: D c= TrivExt D by XBOOLE_1:7;
assume A2: W in the carrier of X ; :: thesis: (Proj (TrivExt D)) . W = (Proj D) . W
then reconsider p = W as Point of X ;
(proj D) . p in D ;
then reconsider A = (Proj D) . W as Element of TrivExt D by A1;
W in A by A2, Def1;
hence (Proj (TrivExt D)) . W = (Proj D) . W by Th29; :: thesis: verum