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' and
A3: ((Proj D) * R) . xx <> ((Proj D) * R) . xx' ; :: thesis: contradiction
( xx in the carrier of X & xx' in the carrier of X ) by A2, A3, Th78;
then ( R . xx = xx & R . xx' = xx' ) by A1, Def19;
then A4: ( (Proj D) . xx = ((Proj D) * R) . xx & (Proj D) . xx' = ((Proj D) * R) . xx' ) by FUNCT_2:21;
( (Proj (TrivExt D)) . xx = (Proj D) . xx & (Proj (TrivExt D)) . xx' = (Proj D) . xx' ) by A2, A3, Th76, Th78;
hence contradiction by A2, A3, A4; :: 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 FF = (Proj D) * R as continuous Function of XX,(space D) ;
reconsider GG = ((Proj D) * R) " G as a_neighborhood of (Proj (TrivExt D)) " {W} by A5, Th20, Th39;
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 W in the carrier of (space D) ; :: thesis: F'' . W = W
then W' in the carrier of X by A6, Th79;
then ( W' = R . W' & (Proj D) . W' = (Proj (TrivExt D)) . W' ) by A1, Def19, Th76;
then ( F' . W = (F * (Proj (TrivExt D))) . W' & W = ((Proj D) * R) . W' ) by A6, FUNCT_2:21;
hence F'' . W = W by A5; :: thesis: verum

end;