let n be Nat; :: thesis: for P being Subset of (TOP-REAL n)
for w1, w2, w3, w4, w5, w6, w7 being Point of (TOP-REAL n) st w1 in P & w2 in P & w3 in P & w4 in P & w5 in P & w6 in P & w7 in P & LSeg (w1,w2) c= P & LSeg (w2,w3) c= P & LSeg (w3,w4) c= P & LSeg (w4,w5) c= P & LSeg (w5,w6) c= P & LSeg (w6,w7) c= P holds
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w7 = h . 1 )
let P be Subset of (TOP-REAL n); :: thesis: for w1, w2, w3, w4, w5, w6, w7 being Point of (TOP-REAL n) st w1 in P & w2 in P & w3 in P & w4 in P & w5 in P & w6 in P & w7 in P & LSeg (w1,w2) c= P & LSeg (w2,w3) c= P & LSeg (w3,w4) c= P & LSeg (w4,w5) c= P & LSeg (w5,w6) c= P & LSeg (w6,w7) c= P holds
ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w7 = h . 1 )
let w1, w2, w3, w4, w5, w6, w7 be Point of (TOP-REAL n); :: thesis: ( w1 in P & w2 in P & w3 in P & w4 in P & w5 in P & w6 in P & w7 in P & LSeg (w1,w2) c= P & LSeg (w2,w3) c= P & LSeg (w3,w4) c= P & LSeg (w4,w5) c= P & LSeg (w5,w6) c= P & LSeg (w6,w7) c= P implies ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w7 = h . 1 ) )
assume that
A1: w1 in P and
A2: ( w2 in P & w3 in P & w4 in P & w5 in P & w6 in P & w7 in P & LSeg (w1,w2) c= P & LSeg (w2,w3) c= P & LSeg (w3,w4) c= P & LSeg (w4,w5) c= P & LSeg (w5,w6) c= P & LSeg (w6,w7) c= P ) ; :: thesis: ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w7 = h . 1 )
( ex h2 being Function of I[01],((TOP-REAL n) | P) st
( h2 is continuous & w1 = h2 . 0 & w4 = h2 . 1 ) & ex h4 being Function of I[01],((TOP-REAL n) | P) st
( h4 is continuous & w4 = h4 . 0 & w7 = h4 . 1 ) ) by A1, A2, Th26;
hence ex h being Function of I[01],((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w7 = h . 1 ) by A1, Th24; :: thesis: verum