let G be non empty TopSpace; :: thesis: for w1, w2, w3 being Point of G
for h1, h2 being Function of I[01] ,G st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01] ,G st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )
let w1, w2, w3 be Point of G; :: thesis: for h1, h2 being Function of I[01] ,G st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01] ,G st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )
let h1, h2 be Function of I[01] ,G; :: thesis: ( h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 implies ex h3 being Function of I[01] ,G st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) )
assume A1: ( h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 ) ; :: thesis: ex h3 being Function of I[01] ,G st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )
then w1,w2 are_connected by Def1;
then reconsider g1 = h1 as Path of w1,w2 by A1, Def2;
w2,w3 are_connected by A1, Def1;
then reconsider g2 = h2 as Path of w2,w3 by A1, Def2;
set P1 = g1;
set P2 = g2;
set p1 = w1;
set p3 = w3;
ex P0 being Path of w1,w3 st
( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01]
for t' being Real st t = t' holds
( ( 0 <= t' & t' <= 1 / 2 implies P0 . t = g1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies P0 . t = g2 . ((2 * t') - 1) ) ) ) )
proof
set e1 = P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) );
set e2 = P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) );
set E1 = g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ));
set E2 = g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ));
set f = (g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )));
A2: dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) by FUNCT_2:def 1
.= [.0 ,(1 / 2).] by TOPMETR:25 ;
A3: dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) = the carrier of (Closed-Interval-TSpace (1 / 2),1) by FUNCT_2:def 1
.= [.(1 / 2),1.] by TOPMETR:25 ;
A4: ( dom g1 = the carrier of I[01] & dom g2 = the carrier of I[01] ) by FUNCT_2:def 1;
then A5: rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) c= dom g1 by TOPMETR:27;
rng (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) c= the carrier of (Closed-Interval-TSpace 0 ,1) ;
then A6: dom (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) = dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) by A4, RELAT_1:46, TOPMETR:27;
A7: dom ((g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) = (dom (g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )))) \/ (dom (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) by FUNCT_4:def 1
.= [.0 ,(1 / 2).] \/ [.(1 / 2),1.] by A2, A3, A5, A6, RELAT_1:46
.= the carrier of I[01] by BORSUK_1:83, XXREAL_1:174 ;
A8: for t' being Real st 0 <= t' & t' <= 1 / 2 holds
(g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t' = g1 . (2 * t')
proof
let t' be Real; :: thesis: ( 0 <= t' & t' <= 1 / 2 implies (g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t' = g1 . (2 * t') )
assume A9: ( 0 <= t' & t' <= 1 / 2 ) ; :: thesis: (g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t' = g1 . (2 * t')
dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) by FUNCT_2:def 1;
then dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) = [.0 ,(1 / 2).] by TOPMETR:25
.= { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by RCOMP_1:def 1 ;
then A10: t' in dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) by A9;
then reconsider s = t' as Point of (Closed-Interval-TSpace 0 ,(1 / 2)) ;
reconsider r1 = (#) 0 ,1, r2 = 0 ,1 (#) as Real by TREAL_1:8;
(P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . s = (((r2 - r1) / ((1 / 2) - 0 )) * t') + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0 )) by TREAL_1:14
.= 2 * t' by TREAL_1:8 ;
hence (g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t' = g1 . (2 * t') by A10, FUNCT_1:23; :: thesis: verum
end;
not 0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
proof
assume 0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ; :: thesis: contradiction
then ex rr being Real st
( rr = 0 & 1 / 2 <= rr & rr <= 1 ) ;
hence contradiction ; :: thesis: verum
end;
then not 0 in dom (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) by A3, A6, RCOMP_1:def 1;
then A11: ((g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) . 0 = (g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . 0 by FUNCT_4:12
.= g1 . (2 * 0 ) by A8
.= w1 by A1 ;
rng ((g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) c= (rng (g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )))) \/ (rng (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) by FUNCT_4:18;
then rng ((g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) c= the carrier of G by XBOOLE_1:1;
then reconsider f = (g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) as Function of I[01] ,G by A7, FUNCT_2:def 1, RELSET_1:11;
reconsider T1 = Closed-Interval-TSpace 0 ,(1 / 2), T2 = Closed-Interval-TSpace (1 / 2),1 as SubSpace of I[01] by TOPMETR:27, TREAL_1:6;
A12: P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ) is continuous by TREAL_1:15;
A13: P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ) is continuous by TREAL_1:15;
reconsider ff = g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) as Function of T1,G by TOPMETR:27;
A14: g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) is Function of the carrier of (Closed-Interval-TSpace (1 / 2),1),the carrier of G by TOPMETR:27;
reconsider gg = g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) as Function of T2,G by TOPMETR:27;
1 / 2 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then reconsider pol = 1 / 2 as Point of I[01] by BORSUK_1:83, RCOMP_1:def 1;
A15: ( ff is continuous & gg is continuous ) by A1, A12, A13, TOPMETR:27;
A16: [#] T1 = [.0 ,(1 / 2).] by TOPMETR:25;
A17: [#] T2 = [.(1 / 2),1.] by TOPMETR:25;
then A18: ([#] T1) \/ ([#] T2) = [#] I[01] by A16, BORSUK_1:83, XXREAL_1:174;
A19: for t' being Real st 1 / 2 <= t' & t' <= 1 holds
(g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t' = g2 . ((2 * t') - 1)
proof
let t' be Real; :: thesis: ( 1 / 2 <= t' & t' <= 1 implies (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t' = g2 . ((2 * t') - 1) )
assume A20: ( 1 / 2 <= t' & t' <= 1 ) ; :: thesis: (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t' = g2 . ((2 * t') - 1)
dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) = the carrier of (Closed-Interval-TSpace (1 / 2),1) by FUNCT_2:def 1;
then dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) = [.(1 / 2),1.] by TOPMETR:25
.= { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by RCOMP_1:def 1 ;
then A21: t' in dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) by A20;
then reconsider s = t' as Point of (Closed-Interval-TSpace (1 / 2),1) ;
reconsider r1 = (#) 0 ,1, r2 = 0 ,1 (#) as Real by TREAL_1:8;
(P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) . s = (((r2 - r1) / (1 - (1 / 2))) * t') + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2))) by TREAL_1:14
.= (2 * t') - 1 by TREAL_1:8 ;
hence (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t' = g2 . ((2 * t') - 1) by A21, FUNCT_1:23; :: thesis: verum
end;
A22: ff . (1 / 2) = g2 . ((2 * (1 / 2)) - 1) by A1, A8
.= gg . pol by A19 ;
A23: ([#] T1) /\ ([#] T2) = {pol} by A16, A17, XXREAL_1:418;
R^1 is T_2 by PCOMPS_1:38, TOPMETR:def 7;
then ( T1 is compact & T2 is compact & I[01] is T_2 & ff . pol = gg . pol ) by A22, HEINE:11;
then reconsider f = f as continuous Function of I[01] ,G by A15, A18, A23, COMPTS_1:29;
1 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;
then 1 in dom (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) by A3, A6, RCOMP_1:def 1;
then A24: f . 1 = (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . 1 by FUNCT_4:14
.= g2 . ((2 * 1) - 1) by A19
.= w3 by A1 ;
then w1,w3 are_connected by A11, Def1;
then reconsider f = f as Path of w1,w3 by A11, A24, Def2;
for t being Point of I[01]
for t' being Real st t = t' holds
( ( 0 <= t' & t' <= 1 / 2 implies f . t = g1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies f . t = g2 . ((2 * t') - 1) ) )
proof
let t be Point of I[01] ; :: thesis: for t' being Real st t = t' holds
( ( 0 <= t' & t' <= 1 / 2 implies f . t = g1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies f . t = g2 . ((2 * t') - 1) ) )
let t' be Real; :: thesis: ( t = t' implies ( ( 0 <= t' & t' <= 1 / 2 implies f . t = g1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies f . t = g2 . ((2 * t') - 1) ) ) )
assume A25: t = t' ; :: thesis: ( ( 0 <= t' & t' <= 1 / 2 implies f . t = g1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies f . t = g2 . ((2 * t') - 1) ) )
thus ( 0 <= t' & t' <= 1 / 2 implies f . t = g1 . (2 * t') ) :: thesis: ( 1 / 2 <= t' & t' <= 1 implies f . t = g2 . ((2 * t') - 1) )
proof
assume A26: ( 0 <= t' & t' <= 1 / 2 ) ; :: thesis: f . t = g1 . (2 * t')
then t' in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } ;
then A27: t' in [.0 ,(1 / 2).] by RCOMP_1:def 1;
per cases ( t' <> 1 / 2 or t' = 1 / 2 ) ;
suppose A28: t' <> 1 / 2 ; :: thesis: f . t = g1 . (2 * t')
not t' in dom (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
proof
assume t' in dom (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) ; :: thesis: contradiction
then t' in [.0 ,(1 / 2).] /\ [.(1 / 2),1.] by A3, A6, A27, XBOOLE_0:def 4;
then t' in {(1 / 2)} by XXREAL_1:418;
hence contradiction by A28, TARSKI:def 1; :: thesis: verum
end;
then f . t = (g1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t by A25, FUNCT_4:12
.= g1 . (2 * t') by A8, A25, A26 ;
hence f . t = g1 . (2 * t') ; :: thesis: verum
end;
suppose A29: t' = 1 / 2 ; :: thesis: f . t = g1 . (2 * t')
1 / 2 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;
then 1 / 2 in [.(1 / 2),1.] by RCOMP_1:def 1;
then 1 / 2 in the carrier of (Closed-Interval-TSpace (1 / 2),1) by TOPMETR:25;
then t in dom (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) by A14, A25, A29, FUNCT_2:def 1;
then f . t = (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . (1 / 2) by A25, A29, FUNCT_4:14
.= g1 . (2 * t') by A8, A22, A29 ;
hence f . t = g1 . (2 * t') ; :: thesis: verum
end;
end;
end;
thus ( 1 / 2 <= t' & t' <= 1 implies f . t = g2 . ((2 * t') - 1) ) :: thesis: verum
proof
assume A30: ( 1 / 2 <= t' & t' <= 1 ) ; :: thesis: f . t = g2 . ((2 * t') - 1)
then t' in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;
then t' in [.(1 / 2),1.] by RCOMP_1:def 1;
then f . t = (g2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t by A3, A6, A25, FUNCT_4:14
.= g2 . ((2 * t') - 1) by A19, A25, A30 ;
hence f . t = g2 . ((2 * t') - 1) ; :: thesis: verum
end;
end;
hence ex P0 being Path of w1,w3 st
( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01]
for t' being Real st t = t' holds
( ( 0 <= t' & t' <= 1 / 2 implies P0 . t = g1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies P0 . t = g2 . ((2 * t') - 1) ) ) ) ) by A11, A24; :: thesis: verum
end;
then consider P0 being Path of w1,w3 such that
A31: ( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01]
for t' being Real st t = t' holds
( ( 0 <= t' & t' <= 1 / 2 implies P0 . t = g1 . (2 * t') ) & ( 1 / 2 <= t' & t' <= 1 implies P0 . t = g2 . ((2 * t') - 1) ) ) ) ) ;
rng P0 c= (rng g1) \/ (rng g2)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng P0 or x in (rng g1) \/ (rng g2) )
assume x in rng P0 ; :: thesis: x in (rng g1) \/ (rng g2)
then consider z being set such that
A32: ( z in dom P0 & x = P0 . z ) by FUNCT_1:def 5;
dom P0 = the carrier of I[01] by FUNCT_2:def 1;
then reconsider r = z as Real by A32, BORSUK_1:83;
A33: ( 0 <= r & r <= 1 ) by A32, BORSUK_1:83, XXREAL_1:1;
A34: dom g1 = the carrier of I[01] by FUNCT_2:def 1;
A35: dom g2 = the carrier of I[01] by FUNCT_2:def 1;
per cases ( r <= 1 / 2 or r > 1 / 2 ) ;
suppose A39: r > 1 / 2 ; :: thesis: x in (rng g1) \/ (rng g2)
then A40: P0 . z = g2 . ((2 * r) - 1) by A31, A32, A33;
2 * (1 / 2) = 1 ;
then 0 + 1 <= 2 * r by A39, XREAL_1:66;
then A41: 0 <= (2 * r) - 1 by XREAL_1:21;
2 * r <= 2 * 1 by A33, XREAL_1:66;
then 2 * r <= 1 + 1 ;
then (2 * r) - 1 <= 1 by XREAL_1:22;
then (2 * r) - 1 in the carrier of I[01] by A41, BORSUK_1:83, XXREAL_1:1;
then P0 . z in rng g2 by A35, A40, FUNCT_1:def 5;
hence x in (rng g1) \/ (rng g2) by A32, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence ex h3 being Function of I[01] ,G st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) by A31; :: thesis: verum