:: BORSUK_2 semantic presentation

E1: for b1 being real number holds
( ( 0 <= b1 & b1 <= 1 ) iff b1 in the carrier of I[01] )
proof
let c1 be real number ;
E2: c1 is Real by XREAL_0:def 1;
E3: [.0,1.] = { b1 where B is Real : ( 0 <= b1 & b1 <= 1 ) } by RCOMP_1:def 1;
hence ( ( 0 <= c1 & c1 <= 1 ) implies ( c1 in the carrier of I[01] ) ) by E2, BORSUK_1:83;
assume c1 in the carrier of I[01] ;
then consider c2 being Real such that
E4: ( c2 = c1 & 0 <= c2 & c2 <= 1 ) by E3, BORSUK_1:83;
thus ( 0 <= c1 & c1 <= 1 ) by E4;
end;

scheme :: BORSUK_2:sch 1
s1{ F1() -> non empty set , F2() -> set , F3( set ) -> set , P1[ set ] } :
Card { F3(b1) where B is Element of F1() : ( b1 in F2() & P1[b1] ) } <=` Card F2()
provided
proof
consider c1 being Function such that
E2: ( dom c1 = F2() & ( for b1 being set holds
( b1 in F2() implies c1 . b1 = F3(b1) ) ) ) from FUNCT_1:sch 3();
 { F3(b1) where B is Element of F1() : ( b1 in F2() & P1[b1] ) } c= rng c1
proof
let c2 be set ; :: according to TARSKI:def 3
assume c2 in { F3(b1) where B is Element of F1() : ( b1 in F2() & P1[b1] ) } ;
then consider c3 being Element of F1() such that
E3: ( c2 = F3(c3) & c3 in F2() & P1[c3] ) ;
c1 . c3 = c2 by E2, E3;
hence c2 in rng c1 by E2, E3, FUNCT_1:def 5;
end;
hence Card { F3(b1) where B is Element of F1() : ( b1 in F2() & P1[b1] ) } <=` Card F2() by E2, CARD_1:28;
end;

theorem :: BORSUK_2:1
for b1, b2, b3, b4 being non empty TopSpace
for b5 being Function of b1,b2
for b6 being Function of b3,b2 holds
not ( b1 is SubSpace of b4 & b3 is SubSpace of b4 & ([#] b1) \/ ([#] b3) = [#] b4 & b1 is compact & b3 is compact & b4 is_T2 & b5 is continuous & b6 is continuous & ( for b7 being set holds
( b7 in ([#] b1) /\ ([#] b3) implies b5 . b7 = b6 . b7 ) ) & ( for b7 being Function of b4,b2 holds
not ( b7 = b5 +* b6 & b7 is continuous ) ) )
proof
let c1, c2, c3, c4 be non empty TopSpace;
let c5 be Function of c1,c2;
let c6 be Function of c3,c2;
assume that
E2: ( c1 is SubSpace of c4 & c3 is SubSpace of c4 ) and
E3: ([#] c1) \/ ([#] c3) = [#] c4 and
E4: c1 is compact and
E5: c3 is compact and
E6: c4 is_T2 and
E7: c5 is continuous and
E8: c6 is continuous and
E9: for b1 being set holds
( b1 in ([#] c1) /\ ([#] c3) implies c5 . b1 = c6 . b1 ) ;
set c7 = c5 +* c6;
E10: dom c5 = the carrier of c1 by FUNCT_2:def 1
.= [#] c1 ;
E11: dom c6 = the carrier of c3 by FUNCT_2:def 1
.= [#] c3 ;
then E12: dom (c5 +* c6) = [#] c4 by E3, E10, FUNCT_4:def 1
.= the carrier of c4 ;
( (rng c5) \/ (rng c6) c= the carrier of c2 & rng (c5 +* c6) c= (rng c5) \/ (rng c6) ) by FUNCT_4:18;
then rng (c5 +* c6) c= the carrier of c2 by XBOOLE_1:1;
then reconsider c8 = c5 +* c6 as Function of c4,c2 by E12, FUNCT_2:4;
take c8 ;
thus c8 = c5 +* c6 ;
for b1 being Subset of c2 holds
( b1 is closed implies c8 " b1 is closed )
proof
let c9 be Subset of c2;
assume E13: c9 is closed ;
E14: ( c8 " c9 c= dom c8 & dom c8 = (dom c5) \/ (dom c6) ) by FUNCT_4:def 1, RELAT_1:167;
then E15: c8 " c9 = (c8 " c9) /\ (([#] c1) \/ ([#] c3)) by E10, E11, XBOOLE_1:28
.= ((c8 " c9) /\ ([#] c1)) \/ ((c8 " c9) /\ ([#] c3)) by XBOOLE_1:23 ;
E16: for b1 being set holds
( b1 in [#] c1 implies c8 . b1 = c5 . b1 )
proof
let c10 be set ;
assume E17: c10 in [#] c1 ;
now
per cases not ( not c10 in [#] c3 & c10 in [#] c3 ) ;
suppose E18: c10 in [#] c3 ;
then c10 in ([#] c1) /\ ([#] c3) by E17, XBOOLE_0:def 3;
then c5 . c10 = c6 . c10 by E9;
hence c8 . c10 = c5 . c10 by E11, E18, FUNCT_4:14;
end;
suppose not c10 in [#] c3 ;
hence c8 . c10 = c5 . c10 by E11, FUNCT_4:12;
end;
end;
end;
hence c8 . c10 = c5 . c10 ;
end;
now
let c10 be set ;
thus ( c10 in (c8 " c9) /\ ([#] c1) implies c10 in c5 " c9 )
proof
assume c10 in (c8 " c9) /\ ([#] c1) ;
then ( c10 in c8 " c9 & c10 in dom c5 & c10 in [#] c1 ) by E10, XBOOLE_0:def 3;
then ( c8 . c10 in c9 & c10 in dom c5 & c5 . c10 = c8 . c10 ) by E16, FUNCT_1:def 13;
hence c10 in c5 " c9 by FUNCT_1:def 13;
end;
assume c10 in c5 " c9 ;
then ( c10 in dom c5 & c5 . c10 in c9 ) by FUNCT_1:def 13;
then ( c10 in dom c8 & c10 in [#] c1 & c8 . c10 in c9 ) by E14, E16, XBOOLE_0:def 2;
then ( c10 in c8 " c9 & c10 in [#] c1 ) by FUNCT_1:def 13;
hence c10 in (c8 " c9) /\ ([#] c1) by XBOOLE_0:def 3;
end;
then E17: (c8 " c9) /\ ([#] c1) = c5 " c9 by TARSKI:2;
now
let c10 be set ;
thus ( c10 in (c8 " c9) /\ ([#] c3) implies c10 in c6 " c9 )
proof
assume c10 in (c8 " c9) /\ ([#] c3) ;
then ( c10 in c8 " c9 & c10 in dom c6 & c10 in [#] c3 ) by E11, XBOOLE_0:def 3;
then ( c8 . c10 in c9 & c10 in dom c6 & c6 . c10 = c8 . c10 ) by FUNCT_1:def 13, FUNCT_4:14;
hence c10 in c6 " c9 by FUNCT_1:def 13;
end;
assume c10 in c6 " c9 ;
then ( c10 in dom c6 & c6 . c10 in c9 ) by FUNCT_1:def 13;
then ( c10 in dom c8 & c10 in [#] c3 & c8 . c10 in c9 ) by E14, FUNCT_4:14, XBOOLE_0:def 2;
then ( c10 in c8 " c9 & c10 in [#] c3 ) by FUNCT_1:def 13;
hence c10 in (c8 " c9) /\ ([#] c3) by XBOOLE_0:def 3;
end;
then E18: c8 " c9 = (c5 " c9) \/ (c6 " c9) by E15, E17, TARSKI:2;
( c5 " c9 c= [#] c1 & [#] c1 c= [#] c4 ) by E3, XBOOLE_1:7;
then c5 " c9 c= [#] c4 by XBOOLE_1:1;
then reconsider c10 = c5 " c9 as Subset of c4 ;
( c6 " c9 c= [#] c3 & [#] c3 c= [#] c4 ) by E3, XBOOLE_1:7;
then c6 " c9 c= [#] c4 by XBOOLE_1:1;
then reconsider c11 = c6 " c9 as Subset of c4 ;
reconsider c12 = c10 \/ c11 as Subset of c4 ;
reconsider c13 = c5 " c9 as Subset of c1 ;
reconsider c14 = c6 " c9 as Subset of c3 ;
( c13 is closed & c14 is closed ) by E7, E8, E13, PRE_TOPC:def 12;
then ( c13 is compact & c14 is compact ) by E4, E5, COMPTS_1:17;
then ( c10 is compact & c11 is compact ) by E2, BORSUK_1:42;
then c12 is compact by COMPTS_1:19;
hence c8 " c9 is closed by E6, E18, COMPTS_1:16;
end;
hence c8 is continuous by PRE_TOPC:def 12;
end;

registration
let c1 be non empty TopStruct ;
cluster id a1 -> continuous open ;
coherence
( id c1 is open & id c1 is continuous )
proof
thus id c1 is open
proof
let c2 be Subset of c1; :: according to T_0TOPSP:def 2
assume E2: c2 is open ;
(id the carrier of c1) .: c2 = c2 by FUNCT_1:162;
hence (id c1) .: c2 is open by E2, GRCAT_1:def 11;
end;
let c2 be Subset of c1; :: according to PRE_TOPC:def 12
assume E2: c2 is closed ;
(id c1) " c2 = (id the carrier of c1) " c2 by GRCAT_1:def 11
.= c2 by BORSUK_1:4 ;
hence (id c1) " c2 is closed by E2;
end;
end;

registration
let c1 be non empty TopStruct ;
cluster one-to-one continuous Relation of the carrier of a1,the carrier of a1;
existence
ex b1 being Function of c1,c1 st
( b1 is continuous & b1 is one-to-one )
proof
take id c1 ;
thus ( id c1 is continuous & id c1 is one-to-one ) ;
end;
end;

theorem :: BORSUK_2:2
canceled;

theorem :: BORSUK_2:3
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is_homeomorphism implies b3 " is open )
proof
let c1, c2 be non empty TopSpace;
let c3 be Function of c1,c2;
assume c3 is_homeomorphism ;
then E2: ( dom c3 = [#] c1 & rng c3 = [#] c2 & c3 is one-to-one & c3 is continuous ) by TOPS_2:def 5;
let c4 be Subset of c2; :: according to T_0TOPSP:def 2
assume E3: c4 is open ;
c3 " c4 = (c3 " ) .: c4 by E2, TOPS_2:68;
hence (c3 " ) .: c4 is open by E2, E3, TOPS_2:55;
end;

registration
cluster -> real Element of the carrier of I[01] ;
coherence
for b1 being Element of I[01] holds b1 is real
proof
let c1 be Element of I[01] ;
c1 in [.0,1.] by BORSUK_1:83;
hence c1 is real by XREAL_0:def 1;
end;
end;

theorem E2: :: BORSUK_2:4
for b1 being non empty TopSpace
for b2 being Point of b1 holds
ex b3 being Function of I[01] ,b1 st
( b3 is continuous & b3 . 0 = b2 & b3 . 1 = b2 )
proof
let c1 be non empty TopSpace;
let c2 be Point of c1;
take c3 = I[01] --> c2;
thus c3 is continuous ;
c3 = the carrier of I[01] --> c2 by BORSUK_1:def 2;
hence ( c3 . 0 = c2 & c3 . 1 = c2 ) by BORSUK_1:def 17, BORSUK_1:def 18, FUNCOP_1:13;
end;

definition
let c1 be TopStruct ;
let c2, c3 be Point of c1;
pred c2,c3 are_connected means :E3: :: BORSUK_2:def 1
ex b1 being Function of I[01] ,a1 st
( b1 is continuous & b1 . 0 = a2 & b1 . 1 = a3 );
end;

:: deftheorem E3 defines are_connected BORSUK_2:def 1 :
for b1 being TopStruct
for b2, b3 being Point of b1 holds
( b2,b3 are_connected iff ex b4 being Function of I[01] ,b1 st
( b4 is continuous & b4 . 0 = b2 & b4 . 1 = b3 ) );

definition
let c1 be non empty TopSpace;
let c2, c3 be Point of c1;
redefine pred are_connected as c2,c3 are_connected ;
reflexivity
for b1 being Point of c1 holds b1,b1 are_connected
proof
let c4 be Point of c1;
thus ex b1 being Function of I[01] ,c1 st
( b1 is continuous & b1 . 0 = c4 & b1 . 1 = c4 ) by E2; :: according to BORSUK_2:def 1
end;
end;

definition
let c1 be TopStruct ;
let c2, c3 be Point of c1;
assume E4: c2,c3 are_connected ;
mode Path of c2,c3 -> Function of I[01] ,a1 means :E4: :: BORSUK_2:def 2
( a4 is continuous & a4 . 0 = a2 & a4 . 1 = a3 );
existence
ex b1 being Function of I[01] ,c1 st
( b1 is continuous & b1 . 0 = c2 & b1 . 1 = c3 ) by E4, E3;
end;

:: deftheorem E4 defines Path BORSUK_2:def 2 :
for b1 being TopStruct
for b2, b3 being Point of b1 holds
( b2,b3 are_connected implies for b4 being Function of I[01] ,b1 holds
( b4 is Path of b2,b3 iff ( b4 is continuous & b4 . 0 = b2 & b4 . 1 = b3 ) ) );

registration
let c1 be non empty TopSpace;
let c2 be Point of c1;
cluster continuous Path of a2,a2;
existence
ex b1 being Path of c2,c2 st b1 is continuous
proof
set c3 = I[01] --> c2;
E5: I[01] --> c2 = the carrier of I[01] --> c2 by BORSUK_1:def 2;
E6: ( (I[01] --> c2) . 0 = c2 & (I[01] --> c2) . 1 = c2 ) by E5, BORSUK_1:def 17, BORSUK_1:def 18, FUNCOP_1:13;
c2,c2 are_connected ;
then I[01] --> c2 is Path of c2,c2 by E6, E4;
hence ex b1 being Path of c2,c2 st b1 is continuous ;
end;
end;

definition
let c1 be TopStruct ;
attr a1 is arcwise_connected means :E5: :: BORSUK_2:def 3
for b1, b2 being Point of a1 holds b1,b2 are_connected ;
correctness
;
end;

:: deftheorem E5 defines arcwise_connected BORSUK_2:def 3 :
for b1 being TopStruct holds
( b1 is arcwise_connected iff for b2, b3 being Point of b1 holds b2,b3 are_connected );

registration
cluster non empty arcwise_connected TopStruct ;
existence
ex b1 being TopSpace st
( b1 is arcwise_connected & not b1 is empty )
proof
set c1 = I[01] | {0[01] };
E6: the carrier of (I[01] | {0[01] }) = {0[01] } by PRE_TOPC:29;
( 0[01] in the carrier of I[01] & 0[01] in {0[01] } ) by TARSKI:def 1;
then reconsider c2 = 0[01] as Point of (I[01] | {0[01] }) by PRE_TOPC:29;
for b1, b2 being Point of (I[01] | {0[01] }) holds b1,b2 are_connected
proof
let c3, c4 be Point of (I[01] | {0[01] });
E7: ( c3 = c2 & c4 = c2 ) by E6, TARSKI:def 1;
reconsider c5 = I[01] --> c2 as Function of I[01] ,(I[01] | {0[01] }) ;
take c5 ; :: according to BORSUK_2:def 1
thus c5 is continuous ;
c5 = the carrier of I[01] --> c2 by BORSUK_1:def 2;
hence ( c5 . 0 = c3 & c5 . 1 = c4 ) by E7, BORSUK_1:def 17, BORSUK_1:def 18, FUNCOP_1:13;
end;
then I[01] | {0[01] } is arcwise_connected by E5;
hence ex b1 being TopSpace st
( b1 is arcwise_connected & not b1 is empty ) ;
end;
end;

definition
let c1 be arcwise_connected TopStruct ;
let c2, c3 be Point of c1;
redefine mode Path of c2,c3 -> Function of I[01] ,a1 means :E6: :: BORSUK_2:def 4
( a4 is continuous & a4 . 0 = a2 & a4 . 1 = a3 );
compatibility
for b1 being Function of I[01] ,c1 holds
( b1 is Path of c2,c3 iff ( b1 is continuous & b1 . 0 = c2 & b1 . 1 = c3 ) )
proof
c2,c3 are_connected by E5;
hence for b1 being Function of I[01] ,c1 holds
( b1 is Path of c2,c3 iff ( b1 is continuous & b1 . 0 = c2 & b1 . 1 = c3 ) ) by E4;
end;
end;

:: deftheorem E6 defines Path BORSUK_2:def 4 :
for b1 being arcwise_connected TopStruct
for b2, b3 being Point of b1
for b4 being Function of I[01] ,b1 holds
( b4 is Path of b2,b3 iff ( b4 is continuous & b4 . 0 = b2 & b4 . 1 = b3 ) );

registration
let c1 be arcwise_connected TopStruct ;
let c2, c3 be Point of c1;
cluster -> continuous Path of a2,a3;
coherence
for b1 being Path of c2,c3 holds b1 is continuous by E6;
end;

E7: ( 0 in [.0,1.] & 1 in [.0,1.] )
proof
( 0 in { b1 where B is Real : ( 0 <= b1 & b1 <= 1 ) } & 1 in { b1 where B is Real : ( 0 <= b1 & b1 <= 1 ) } ) ;
hence ( 0 in [.0,1.] & 1 in [.0,1.] ) by RCOMP_1:def 1;
end;

theorem E8: :: BORSUK_2:5
for b1 being non empty TopSpace holds
( b1 is arcwise_connected implies b1 is connected )
proof
let c1 be non empty TopSpace;
assume E9: for b1, b2 being Point of c1 holds b1,b2 are_connected ; :: according to BORSUK_2:def 3
for b1, b2 being Point of c1 holds
ex b3 being non empty TopSpace st
( b3 is connected & ex b4 being Function of b3,c1 st
( b4 is continuous & b1 in rng b4 & b2 in rng b4 ) )
proof
let c2, c3 be Point of c1;
now
c2,c3 are_connected by E9;
then consider c4 being Function of I[01] ,c1 such that
E10: c4 is continuous and
E11: ( c2 = c4 . 0 & c3 = c4 . 1 ) by E3;
( 0 in dom c4 & 1 in dom c4 ) by E7, BORSUK_1:83, FUNCT_2:def 1;
then ( c2 in rng c4 & c3 in rng c4 ) by E11, FUNCT_1:def 5;
hence ex b1 being non empty TopSpace st
( b1 is connected & ex b2 being Function of b1,c1 st
( b2 is continuous & c2 in rng b2 & c3 in rng b2 ) ) by E10, TREAL_1:22;
end;
hence ex b1 being non empty TopSpace st
( b1 is connected & ex b2 being Function of b1,c1 st
( b2 is continuous & c2 in rng b2 & c3 in rng b2 ) ) ;
end;
hence c1 is connected by JORDAN1:2;
end;

registration
cluster non empty arcwise_connected -> non empty connected TopStruct ;
coherence
for b1 being non empty TopSpace holds
( b1 is arcwise_connected implies b1 is connected ) by E8;
end;

E9: for b1 being non empty TopSpace
for b2, b3, b4 being Point of b1
for b5, b6 being Function of I[01] ,b1 holds
not ( b5 is continuous & b2 = b5 . 0 & b3 = b5 . 1 & b6 is continuous & b3 = b6 . 0 & b4 = b6 . 1 & ( for b7 being Function of I[01] ,b1 holds
not ( b7 is continuous & b2 = b7 . 0 & b4 = b7 . 1 & rng b7 c= (rng b5) \/ (rng b6) ) ) )
proof
let c1 be non empty TopSpace;
let c2, c3, c4 be Point of c1;
let c5, c6 be Function of I[01] ,c1;
assume E10: ( c5 is continuous & c2 = c5 . 0 & c3 = c5 . 1 & c6 is continuous & c3 = c6 . 0 & c4 = c6 . 1 ) ;
then c2,c3 are_connected by E3;
then reconsider c7 = c5 as Path of c2,c3 by E10, E4;
c3,c4 are_connected by E10, E3;
then reconsider c8 = c6 as Path of c3,c4 by E10, E4;
set c9 = c7;
set c10 = c8;
set c11 = c2;
set c12 = c4;
ex b1 being Path of c2,c4 st
( b1 is continuous & b1 . 0 = c2 & b1 . 1 = c4 & ( for b2 being Point of I[01]
for b3 being Real holds
( b2 = b3 implies ( ( ( 0 <= b3 & b3 <= 1 / 2 ) implies ( b1 . b2 = c7 . (2 * b3) ) ) & ( ( 1 / 2 <= b3 & b3 <= 1 ) implies ( b1 . b2 = c8 . ((2 * b3) - 1) ) ) ) ) ) )
proof
set c13 = P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) );
set c14 = P[01] (1 / 2),1,((#) 0,1),(0,1 (#) );
set c15 = c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ));
set c16 = c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ));
set c17 = (c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ))) +* (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )));
E11: 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 ;
E12: 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 ;
E13: ( dom c7 = the carrier of I[01] & dom c8 = the carrier of I[01] ) by FUNCT_2:def 1;
then E14: rng (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) )) c= dom c7 by TOPMETR:27;
rng (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )) c= the carrier of (Closed-Interval-TSpace 0,1) ;
then E15: dom (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) = dom (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )) by E13, RELAT_1:46, TOPMETR:27;
E16: dom ((c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ))) +* (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )))) = (dom (c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) )))) \/ (dom (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )))) by FUNCT_4:def 1
.= [.0,(1 / 2).] \/ [.(1 / 2),1.] by E11, E12, E14, E15, RELAT_1:46
.= the carrier of I[01] by BORSUK_1:83, TREAL_1:2 ;
E17: for b1 being Real holds
( ( 0 <= b1 & b1 <= 1 / 2 ) implies ( (c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ))) . b1 = c7 . (2 * b1) ) )
proof
let c18 be Real;
assume E18: ( 0 <= c18 & c18 <= 1 / 2 ) ;
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
.= { b1 where B is Real : ( 0 <= b1 & b1 <= 1 / 2 ) } by RCOMP_1:def 1 ;
then E19: c18 in dom (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) )) by E18;
then reconsider c19 = c18 as Point of (Closed-Interval-TSpace 0,(1 / 2)) ;
reconsider c20 = (#) 0,1, c21 = 0,1 (#) as Real by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8;
(P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) )) . c19 = (((c21 - c20) / ((1 / 2) - 0)) * c18) + ((((1 / 2) * c20) - (0 * c21)) / ((1 / 2) - 0)) by TREAL_1:14
.= 2 * c18 by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8 ;
hence (c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ))) . c18 = c7 . (2 * c18) by E19, FUNCT_1:23;
end;
not 0 in { b1 where B is Real : ( 1 / 2 <= b1 & b1 <= 1 ) }
proof
assume 0 in { b1 where B is Real : ( 1 / 2 <= b1 & b1 <= 1 ) } ;
then ex b1 being Real st
( b1 = 0 & 1 / 2 <= b1 & b1 <= 1 ) ;
hence not verum ;
end;
then not 0 in dom (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) by E12, E15, RCOMP_1:def 1;
then E18: ((c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ))) +* (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )))) . 0 = (c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ))) . 0 by FUNCT_4:12
.= c7 . (2 * 0) by E17
.= c2 by E10 ;
E19: rng ((c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ))) +* (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )))) c= (rng (c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) )))) \/ (rng (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )))) by FUNCT_4:18;
rng ((c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ))) +* (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )))) c= the carrier of c1 by E19, XBOOLE_1:1;
then reconsider c18 = (c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ))) +* (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) as Function of I[01] ,c1 by E16, FUNCT_2:def 1, RELSET_1:11;
reconsider c19 = Closed-Interval-TSpace 0,(1 / 2), c20 = Closed-Interval-TSpace (1 / 2),1 as SubSpace of I[01] by TOPMETR:27, TREAL_1:6;
E20: P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ) is continuous by TREAL_1:15;
E21: P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ) is continuous by TREAL_1:15;
reconsider c21 = c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) )) as Function of c19,c1 by FUNCT_2:19, TOPMETR:27;
E22: c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )) is Function of the carrier of (Closed-Interval-TSpace (1 / 2),1),the carrier of c1 by FUNCT_2:19, TOPMETR:27;
reconsider c22 = c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )) as Function of c20,c1 by FUNCT_2:19, TOPMETR:27;
1 / 2 in { b1 where B is Real : ( 0 <= b1 & b1 <= 1 ) } ;
then reconsider c23 = 1 / 2 as Point of I[01] by BORSUK_1:83, RCOMP_1:def 1;
E23: ( c21 is continuous & c22 is continuous ) by E10, E20, E21, TOPMETR:27, TOPS_2:58;
E24: [#] c19 = the carrier of c19
.= [.0,(1 / 2).] by TOPMETR:25 ;
E25: [#] c20 = the carrier of c20
.= [.(1 / 2),1.] by TOPMETR:25 ;
then E26: ([#] c19) \/ ([#] c20) = [.0,1.] by E24, TREAL_1:2
.= [#] I[01] by BORSUK_1:83 ;
E27: for b1 being Real holds
( ( 1 / 2 <= b1 & b1 <= 1 ) implies ( (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) . b1 = c8 . ((2 * b1) - 1) ) )
proof
let c24 be Real;
assume E28: ( 1 / 2 <= c24 & c24 <= 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
.= { b1 where B is Real : ( 1 / 2 <= b1 & b1 <= 1 ) } by RCOMP_1:def 1 ;
then E29: c24 in dom (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )) by E28;
then reconsider c25 = c24 as Point of (Closed-Interval-TSpace (1 / 2),1) ;
reconsider c26 = (#) 0,1, c27 = 0,1 (#) as Real by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8;
(P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )) . c25 = (((c27 - c26) / (1 - (1 / 2))) * c24) + (((1 * c26) - ((1 / 2) * c27)) / (1 - (1 / 2))) by TREAL_1:14
.= (2 * c24) + (- 1) by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8
.= (2 * c24) - 1 ;
hence (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) . c24 = c8 . ((2 * c24) - 1) by E29, FUNCT_1:23;
end;
E28: c21 . (1 / 2) = c8 . ((2 * (1 / 2)) - 1) by E10, E17
.= c22 . c23 by E27 ;
E29: ([#] c19) /\ ([#] c20) = {c23} by E24, E25, TOPMETR2:1;
R^1 is_T2 by PCOMPS_1:38, TOPMETR:def 7;
then ( c19 is compact & c20 is compact & I[01] is_T2 & c21 . c23 = c22 . c23 ) by E28, HEINE:11, TOPMETR:3;
then reconsider c24 = c18 as continuous Function of I[01] ,c1 by E23, E26, E29, TOPMETR2:4;
1 in { b1 where B is Real : ( 1 / 2 <= b1 & b1 <= 1 ) } ;
then 1 in dom (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) by E12, E15, RCOMP_1:def 1;
then E30: c24 . 1 = (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) . 1 by FUNCT_4:14
.= c8 . ((2 * 1) - 1) by E27
.= c4 by E10 ;
then c2,c4 are_connected by E18, E3;
then reconsider c25 = c24 as Path of c2,c4 by E18, E30, E4;
for b1 being Point of I[01]
for b2 being Real holds
( b1 = b2 implies ( ( ( 0 <= b2 & b2 <= 1 / 2 ) implies ( c25 . b1 = c7 . (2 * b2) ) ) & ( ( 1 / 2 <= b2 & b2 <= 1 ) implies ( c25 . b1 = c8 . ((2 * b2) - 1) ) ) ) )
proof
let c26 be Point of I[01] ;
let c27 be Real;
assume E31: c26 = c27 ;
thus ( ( 0 <= c27 & c27 <= 1 / 2 ) implies ( c25 . c26 = c7 . (2 * c27) ) )
proof
assume E32: ( 0 <= c27 & c27 <= 1 / 2 ) ;
then c27 in { b1 where B is Real : ( 0 <= b1 & b1 <= 1 / 2 ) } ;
then E33: c27 in [.0,(1 / 2).] by RCOMP_1:def 1;
per cases not ( not c27 <> 1 / 2 & not c27 = 1 / 2 ) ;
suppose E34: c27 <> 1 / 2 ;
not c27 in dom (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) )))
proof
assume c27 in dom (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) ;
then c27 in [.0,(1 / 2).] /\ [.(1 / 2),1.] by E12, E15, E33, XBOOLE_0:def 3;
then c27 in {(1 / 2)} by TOPMETR2:1;
hence not verum by E34, TARSKI:def 1;
end;
then c25 . c26 = (c7 * (P[01] 0,(1 / 2),((#) 0,1),(0,1 (#) ))) . c26 by E31, FUNCT_4:12
.= c7 . (2 * c27) by E17, E31, E32 ;
hence c25 . c26 = c7 . (2 * c27) ;
end;
suppose E34: c27 = 1 / 2 ;
1 / 2 in { b1 where B is Real : ( 1 / 2 <= b1 & b1 <= 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 c26 in dom (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) by E22, E31, E34, FUNCT_2:def 1;
then c25 . c26 = (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) . (1 / 2) by E31, E34, FUNCT_4:14
.= c7 . (2 * c27) by E17, E28, E34 ;
hence c25 . c26 = c7 . (2 * c27) ;
end;
end;
end;
thus ( ( 1 / 2 <= c27 & c27 <= 1 ) implies ( c25 . c26 = c8 . ((2 * c27) - 1) ) )
proof
assume E32: ( 1 / 2 <= c27 & c27 <= 1 ) ;
then c27 in { b1 where B is Real : ( 1 / 2 <= b1 & b1 <= 1 ) } ;
then c27 in [.(1 / 2),1.] by RCOMP_1:def 1;
then c25 . c26 = (c8 * (P[01] (1 / 2),1,((#) 0,1),(0,1 (#) ))) . c26 by E12, E15, E31, FUNCT_4:14
.= c8 . ((2 * c27) - 1) by E27, E31, E32 ;
hence c25 . c26 = c8 . ((2 * c27) - 1) ;
end;
end;
hence ex b1 being Path of c2,c4 st
( b1 is continuous & b1 . 0 = c2 & b1 . 1 = c4 & ( for b2 being Point of I[01]
for b3 being Real holds
( b2 = b3 implies ( ( ( 0 <= b3 & b3 <= 1 / 2 ) implies ( b1 . b2 = c7 .