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

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 17 :: thesis: space D is_a_retract_of space (TrivExt D)

A5: F * (Proj (TrivExt D)) = (Proj D) * R by EQREL_1:56;

reconsider F = F as Function of (space (TrivExt D)),(space D) ;

F is continuous

take F9 ; :: according to BORSUK_1:def 17 :: thesis: F9 is being_a_retraction

let W be Point of (space (TrivExt D)); :: according to BORSUK_1:def 16 :: 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 Th29;

assume A7: W in the carrier of (space D) ; :: thesis: F9 . W = W

then W9 in the carrier of X by A6, Th36;

then A8: W9 = R . W9 by A1;

A9: F9 . W = (F * (Proj (TrivExt D))) . W9 by A6, FUNCT_2:15;

(Proj D) . W9 = (Proj (TrivExt D)) . W9 by A6, A7, Th33, Th36;

hence F9 . W = W by A5, A6, A8, A9, FUNCT_2:15; :: thesis: verum

end;now :: thesis: for xx, xx9 being Point of XX holds

( not (Proj (TrivExt D)) . xx = (Proj (TrivExt D)) . xx9 or not ((Proj D) * R) . xx <> ((Proj D) * R) . xx9 )

then consider F being Function of the carrier of (space (TrivExt D)), the carrier of (space D) such that ( not (Proj (TrivExt D)) . xx = (Proj (TrivExt D)) . xx9 or not ((Proj D) * R) . xx <> ((Proj D) * R) . xx9 )

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, Th35;

then R . xx = xx by A1;

then A3: (Proj D) . xx = ((Proj D) * R) . xx by FUNCT_2:15;

xx9 in the carrier of X by A2, Th35;

then A4: R . xx9 = xx9 by A1;

( (Proj (TrivExt D)) . xx = (Proj D) . xx & (Proj (TrivExt D)) . xx9 = (Proj D) . xx9 ) by A2, Th33, Th35;

hence contradiction by A2, A4, A3, FUNCT_2:15; :: thesis: verum

end;xx in the carrier of X by A2, Th35;

then R . xx = xx by A1;

then A3: (Proj D) . xx = ((Proj D) * R) . xx by FUNCT_2:15;

xx9 in the carrier of X by A2, Th35;

then A4: R . xx9 = xx9 by A1;

( (Proj (TrivExt D)) . xx = (Proj D) . xx & (Proj (TrivExt D)) . xx9 = (Proj D) . xx9 ) by A2, Th33, Th35;

hence contradiction by A2, A4, A3, FUNCT_2:15; :: thesis: verum

A5: F * (Proj (TrivExt D)) = (Proj D) * R by EQREL_1:56;

reconsider F = F as Function of (space (TrivExt D)),(space D) ;

F is continuous

proof

then reconsider F9 = F as continuous Function of (space (TrivExt D)),(space D) ;
let W be Point of (space (TrivExt D)); :: 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 GG = ((Proj D) * R) " G as a_neighborhood of (Proj (TrivExt D)) " {W} by A5, Th4, EQREL_1:57;

reconsider V9 = (Proj (TrivExt D)) .: GG as a_neighborhood of W by Th38;

take V = V9; :: thesis: F .: V c= G

F .: V = ((Proj D) * R) .: GG by A5, RELAT_1:126;

hence F .: V c= G by FUNCT_1:75; :: 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 GG = ((Proj D) * R) " G as a_neighborhood of (Proj (TrivExt D)) " {W} by A5, Th4, EQREL_1:57;

reconsider V9 = (Proj (TrivExt D)) .: GG as a_neighborhood of W by Th38;

take V = V9; :: thesis: F .: V c= G

F .: V = ((Proj D) * R) .: GG by A5, RELAT_1:126;

hence F .: V c= G by FUNCT_1:75; :: thesis: verum

take F9 ; :: according to BORSUK_1:def 17 :: thesis: F9 is being_a_retraction

let W be Point of (space (TrivExt D)); :: according to BORSUK_1:def 16 :: 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 Th29;

assume A7: W in the carrier of (space D) ; :: thesis: F9 . W = W

then W9 in the carrier of X by A6, Th36;

then A8: W9 = R . W9 by A1;

A9: F9 . W = (F * (Proj (TrivExt D))) . W9 by A6, FUNCT_2:15;

(Proj D) . W9 = (Proj (TrivExt D)) . W9 by A6, A7, Th33, Th36;

hence F9 . W = W by A5, A6, A8, A9, FUNCT_2:15; :: thesis: verum