let n be Element of 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, Th45;
hence ex h being Function of I[01] ,((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w7 = h . 1 ) by A1, Th43; :: thesis: verum