let XX be non empty TopSpace; :: thesis: for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)
let X be non empty closed SubSpace of XX; :: thesis: for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)
let D be DECOMPOSITION of X; :: thesis: ( X is_an_SDR_of XX implies space D is_an_SDR_of space (TrivExt D) )
given CH1 being continuous Function of [:XX,I[01]:],XX such that A1: for A being Point of XX holds
( CH1 . [A,0[01]] = A & CH1 . [A,1[01]] in the carrier of X & ( A in the carrier of X implies for T being Point of I[01] holds CH1 . [A,T] = A ) ) ; :: according to BORSUK_1:def 18 :: thesis: space D is_an_SDR_of space (TrivExt D)
the carrier of [:XX,I[01]:] = [: the carrier of XX, the carrier of I[01]:] by Def2;
then reconsider II = [:(Proj (TrivExt D)),(id the carrier of I[01]):] as Function of the carrier of [:XX,I[01]:], the carrier of [:(space (TrivExt D)),I[01]:] by Def2;

now :: thesis: for xx, xx9 being Point of [:XX,I[01]:] holds
( not II . xx = II . xx9 or not ((Proj (TrivExt D)) * CH1) . xx <> ((Proj (TrivExt D)) * CH1) . xx9 )

given xx, xx9 being Point of [:XX,I[01]:] such that A2: II . xx = II . xx9 and
A3: ((Proj (TrivExt D)) * CH1) . xx <> ((Proj (TrivExt D)) * CH1) . xx9 ; :: thesis: contradiction
A4: ( ((Proj (TrivExt D)) * CH1) . xx = (Proj (TrivExt D)) . (CH1 . xx) & ((Proj (TrivExt D)) * CH1) . xx9 = (Proj (TrivExt D)) . (CH1 . xx9) ) by FUNCT_2:15;
consider x being Point of XX, t being Point of I[01] such that
A5: xx = [x,t] by Th10;
consider x9 being Point of XX, t9 being Point of I[01] such that
A6: xx9 = [x9,t9] by Th10;
A7: ( II . (x,t) = [((Proj (TrivExt D)) . x),t] & II . (x9,t9) = [((Proj (TrivExt D)) . x9),t9] ) by EQREL_1:58;
then ( t = t9 & (Proj (TrivExt D)) . x = (Proj (TrivExt D)) . x9 ) by A2, A5, A6, XTUPLE_0:1;
then ( CH1 . xx = x & CH1 . xx9 = x9 ) by A1, A3, A5, A6, Th35;
hence contradiction by A2, A3, A5, A6, A7, A4, XTUPLE_0:1; :: thesis: verum

end;

then consider THETA being Function of the carrier of [:(space (TrivExt D)),I[01]:], the carrier of (space (TrivExt D)) such that
A8: (Proj (TrivExt D)) * CH1 = THETA * II by EQREL_1:56;
reconsider THETA = THETA as Function of [:(space (TrivExt D)),I[01]:],(space (TrivExt D)) ;
THETA is continuous

proof

let WT be Point of [:(space (TrivExt D)),I[01]:]; :: according to BORSUK_1:def 1 :: thesis: for G being a_neighborhood of THETA . WT ex H being a_neighborhood of WT st THETA .: H c= G
reconsider xt9 = WT as Element of [: the carrier of (space (TrivExt D)), the carrier of I[01]:] by Def2;
let G be a_neighborhood of THETA . WT; :: thesis: ex H being a_neighborhood of WT st THETA .: H c= G
reconsider FF = (Proj (TrivExt D)) * CH1 as continuous Function of [:XX,I[01]:],(space (TrivExt D)) ;
consider W being Point of (space (TrivExt D)), T being Point of I[01] such that
A9: WT = [W,T] by Th10;
II " {xt9} = [:((Proj (TrivExt D)) " {W}),{T}:] by A9, EQREL_1:60;
then reconsider GG = FF " G as a_neighborhood of [:((Proj (TrivExt D)) " {W}),{T}:] by A8, Th4, EQREL_1:57;
W in the carrier of (space (TrivExt D)) ;
then A10: W in TrivExt D by Def7;
then (Proj (TrivExt D)) " {W} = W by EQREL_1:66;
then (Proj (TrivExt D)) " {W} is compact by A10, Def12;
then consider U being a_neighborhood of (Proj (TrivExt D)) " {W}, V being a_neighborhood of T such that
A11: [:U,V:] c= GG by Th25;
reconsider H9 = (Proj (TrivExt D)) .: U as a_neighborhood of W by Th38;
reconsider H99 = [:H9,V:] as a_neighborhood of WT by A9;
take H = H99; :: thesis: THETA .: H c= G
II .: [:U,V:] = [:((Proj (TrivExt D)) .: U),V:] by EQREL_1:59;
then A12: ( ((Proj (TrivExt D)) * CH1) .: GG c= G & THETA .: H = ((Proj (TrivExt D)) * CH1) .: [:U,V:] ) by A8, FUNCT_1:75, RELAT_1:126;
((Proj (TrivExt D)) * CH1) .: [:U,V:] c= ((Proj (TrivExt D)) * CH1) .: GG by A11, RELAT_1:123;
hence THETA .: H c= G by A12; :: thesis: verum

end;

then reconsider THETA9 = THETA as continuous Function of [:(space (TrivExt D)),I[01]:],(space (TrivExt D)) ;
take THETA99 = THETA9; :: according to BORSUK_1:def 18 :: thesis: for A being Point of (space (TrivExt D)) holds
( THETA99 . [A,0[01]] = A & THETA99 . [A,1[01]] in the carrier of (space D) & ( A in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [A,T] = A ) )
let W be Point of (space (TrivExt D)); :: thesis: ( THETA99 . [W,0[01]] = W & THETA99 . [W,1[01]] in the carrier of (space D) & ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W ) )
consider W9 being Point of XX such that
A13: (Proj (TrivExt D)) . W9 = W by Th29;
II . (W9,0[01]) = [W,0[01]] by A13, EQREL_1:58;
then A14: (THETA9 * II) . [W9,0[01]] = THETA9 . [W,0[01]] by FUNCT_2:15;
CH1 . (W9,0[01]) = W9 by A1;
hence THETA99 . [W,0[01]] = W by A8, A13, A14, FUNCT_2:15; :: thesis: ( THETA99 . [W,1[01]] in the carrier of (space D) & ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W ) )
A15: CH1 . [W9,1[01]] in the carrier of X by A1;
II . (W9,1[01]) = [W,1[01]] by A13, EQREL_1:58;
then A16: (THETA9 * II) . [W9,1[01]] = THETA9 . [W,1[01]] by FUNCT_2:15;
(THETA9 * II) . [W9,1[01]] = (Proj (TrivExt D)) . (CH1 . [W9,1[01]]) by A8, FUNCT_2:15;
hence THETA99 . [W,1[01]] in the carrier of (space D) by A16, A15, Th37; :: thesis: ( W in the carrier of (space D) implies for T being Point of I[01] holds THETA99 . [W,T] = W )
assume A17: W in the carrier of (space D) ; :: thesis: for T being Point of I[01] holds THETA99 . [W,T] = W
let T be Point of I[01]; :: thesis: THETA99 . [W,T] = W
II . (W9,T) = [W,T] by A13, EQREL_1:58;
then A18: (THETA9 * II) . [W9,T] = THETA9 . [W,T] by FUNCT_2:15;
CH1 . (W9,T) = W9 by A1, A13, A17, Th36;
hence THETA99 . [W,T] = W by A8, A13, A18, FUNCT_2:15; :: thesis: verum