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, xx' being Point of XX such that A2: ( (Proj (TrivExt D)) . xx = (Proj (TrivExt D)) . xx' & ((Proj D) * R) . xx <> ((Proj D) * R) . xx' ) ; :: 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;
xx' in the carrier of X by A2, Th78;
then A4: R . xx' = xx' by A1, Def19;
( (Proj (TrivExt D)) . xx = (Proj D) . xx & (Proj (TrivExt D)) . xx' = (Proj D) . xx' ) 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 Th19;
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, Th20, Th39;
reconsider FF = (Proj D) * R as continuous Function of XX,(space D) ;
reconsider V' = (Proj (TrivExt D)) .: GG as a_neighborhood of W by Th81;
take V = V'; :: 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 F' = F as continuous Function of (space (TrivExt D)),(space D) ;
take F'' = F'; :: according to BORSUK_1:def 20 :: thesis: F'' 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 F'' . W = W )
consider W' being Point of XX such that
A6: (Proj (TrivExt D)) . W' = W by Th71;
assume A7: W in the carrier of (space D) ; :: thesis: F'' . W = W
then W' in the carrier of X by A6, Th79;
then A8: W' = R . W' by A1, Def19;
A9: F' . W = (F * (Proj (TrivExt D))) . W' by A6, FUNCT_2:21;
(Proj D) . W' = (Proj (TrivExt D)) . W' by A6, A7, Th76, Th79;
hence F'' . W = W by A5, A6, A8, A9, FUNCT_2:21; :: thesis: verum

end;