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 e being set st e in the carrier of X holds

(Proj (TrivExt D)) . e in the carrier of (space D)

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

for e being set st e in the carrier of X holds

(Proj (TrivExt D)) . e in the carrier of (space D)

let D be non empty a_partition of the carrier of X; :: thesis: for e being set st e in the carrier of X holds

(Proj (TrivExt D)) . e in the carrier of (space D)

let e be set ; :: thesis: ( e in the carrier of X implies (Proj (TrivExt D)) . e in the carrier of (space D) )

assume A1: e in the carrier of X ; :: thesis: (Proj (TrivExt D)) . e in the carrier of (space D)

then reconsider x = e as Point of X ;

the carrier of X c= the carrier of XX by Th1;

then (Proj D) . x = (Proj (TrivExt D)) . x by A1, Th33;

hence (Proj (TrivExt D)) . e in the carrier of (space D) ; :: thesis: verum

for D being non empty a_partition of the carrier of X

for e being set st e in the carrier of X holds

(Proj (TrivExt D)) . e in the carrier of (space D)

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

for e being set st e in the carrier of X holds

(Proj (TrivExt D)) . e in the carrier of (space D)

let D be non empty a_partition of the carrier of X; :: thesis: for e being set st e in the carrier of X holds

(Proj (TrivExt D)) . e in the carrier of (space D)

let e be set ; :: thesis: ( e in the carrier of X implies (Proj (TrivExt D)) . e in the carrier of (space D) )

assume A1: e in the carrier of X ; :: thesis: (Proj (TrivExt D)) . e in the carrier of (space D)

then reconsider x = e as Point of X ;

the carrier of X c= the carrier of XX by Th1;

then (Proj D) . x = (Proj (TrivExt D)) . x by A1, Th33;

hence (Proj (TrivExt D)) . e in the carrier of (space D) ; :: thesis: verum