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_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)
let X be non empty closed SubSpace of XX; :: thesis: for D being DECOMPOSITION of X st X is_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)
let D be DECOMPOSITION of X; :: thesis: ( X is_a_retract_of XX implies space D is_a_retract_of space (TrivExt D) )
thus ( X is_a_retract_of XX implies space D is_a_retract_of space (TrivExt D) ) :: thesis: verum

proof

given R being continuous Function of XX,X such that A1: R is being_a_retraction ; :: according to BORSUK_1:def 20 :: thesis: space D is_a_retract_of space (TrivExt D)

now

given xx, xx9 being Point of XX such that A2: ( (Proj (TrivExt D)) . xx = (Proj (TrivExt D)) . xx9 & ((Proj D) * R) . xx <> ((Proj D) * R) . xx9 ) ; :: thesis: contradiction
xx in the carrier of X by A2, Th78;
then R . xx = xx by A1, Def19;
then A3: (Proj D) . xx = ((Proj D) * R) . xx by FUNCT_2:21;
xx9 in the carrier of X by A2, Th78;
then A4: R . xx9 = xx9 by A1, Def19;
( (Proj (TrivExt D)) . xx = (Proj D) . xx & (Proj (TrivExt D)) . xx9 = (Proj D) . xx9 ) by A2, Th76, Th78;
hence contradiction by A2, A4, A3, FUNCT_2:21; :: thesis: verum

end;

then consider F being Function of the carrier of (space (TrivExt D)), the carrier of (space D) such that
A5: F * (Proj (TrivExt D)) = (Proj D) * R by EQREL_1:65;
reconsider F = F as Function of (space (TrivExt D)),(space D) ;
F is continuous

proof

let W be Point of (space (TrivExt D)); :: 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 GG = ((Proj D) * R) " G as a_neighborhood of (Proj (TrivExt D)) " {W} by A5, EQREL_1:66, Th39;
reconsider V9 = (Proj (TrivExt D)) .: GG as a_neighborhood of W by Th81;
take V = V9; :: thesis: F .: V c= G
F .: V = ((Proj D) * R) .: GG by A5, RELAT_1:159;
hence F .: V c= G by FUNCT_1:145; :: thesis: verum

end;

then reconsider F9 = F as continuous Function of (space (TrivExt D)),(space D) ;
take F9 ; :: according to BORSUK_1:def 20 :: thesis: F9 is being_a_retraction
let W be Point of (space (TrivExt D)); :: according to BORSUK_1:def 19 :: thesis: ( W in the carrier of (space D) implies F9 . W = W )
consider W9 being Point of XX such that
A6: (Proj (TrivExt D)) . W9 = W by Th71;
assume A7: W in the carrier of (space D) ; :: thesis: F9 . W = W
then W9 in the carrier of X by A6, Th79;
then A8: W9 = R . W9 by A1, Def19;
A9: F9 . W = (F * (Proj (TrivExt D))) . W9 by A6, FUNCT_2:21;
(Proj D) . W9 = (Proj (TrivExt D)) . W9 by A6, A7, Th76, Th79;
hence F9 . W = W by A5, A6, A8, A9, FUNCT_2:21; :: thesis: verum

end;