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

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