reconsider F = proj D as Function of X,(space D) by Def7;

A1: the carrier of (space D) = D by Def7;

F is continuous

A1: the carrier of (space D) = D by Def7;

F is continuous

proof

hence
proj D is continuous Function of X,(space D)
; :: thesis: verum
let W be Point of X; :: according to BORSUK_1:def 1 :: 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, EQREL_1:61;

F . W in Int G by CONNSP_2:def 1;

then W in F " (Int G) by FUNCT_2:38;

then A2: W in union (Int G) by A1, EQREL_1:67;

Int G in the topology of (space D) by PRE_TOPC:def 2;

then union (Int G) in the topology of X by A1, Th27;

then H is open ;

then W in Int H by A2, TOPS_1:23;

then W in Int (F " (Int G)) by A1, EQREL_1:67;

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:75, TOPS_1:16;

hence F .: N c= G ; :: thesis: verum

end;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, EQREL_1:61;

F . W in Int G by CONNSP_2:def 1;

then W in F " (Int G) by FUNCT_2:38;

then A2: W in union (Int G) by A1, EQREL_1:67;

Int G in the topology of (space D) by PRE_TOPC:def 2;

then union (Int G) in the topology of X by A1, Th27;

then H is open ;

then W in Int H by A2, TOPS_1:23;

then W in Int (F " (Int G)) by A1, EQREL_1:67;

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:75, TOPS_1:16;

hence F .: N c= G ; :: thesis: verum