reconsider F = proj D as Function of X,(space D) by Def10;
A1: the carrier of (space D) = D by Def10;
F is continuous
proof
let W be Point of X; :: according to BORSUK_1:def 3 :: thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let G be a_neighborhood of F . W; :: thesis: ex H being a_neighborhood of W st F .: H c= G
reconsider H = union (Int G) as Subset of X by A1, Th25;
F . W in Int G by CONNSP_2:def 1;
then W in F " (Int G) by FUNCT_2:46;
then A2: W in union (Int G) by A1, Th31;
Int G in the topology of (space D) by PRE_TOPC:def 5;
then union (Int G) in the topology of X by A1, Th69;
then H is open by PRE_TOPC:def 5;
then W in Int H by A2, TOPS_1:55;
then W in Int (F " (Int G)) by A1, Th31;
then reconsider N = F " (Int G) as a_neighborhood of W by CONNSP_2:def 1;
take N ; :: thesis: F .: N c= G
( F .: N c= Int G & Int G c= G ) by FUNCT_1:145, TOPS_1:44;
hence F .: N c= G by XBOOLE_1:1; :: thesis: verum
end;
hence proj D is continuous Function of X,(space D) ; :: thesis: verum