:: 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 c= the carrier of c2 & rng c6 c= the carrier of c2 ) by RELSET_1:12;
then ( (rng c5) \/ (rng c6) c= the carrier of c2 & rng (c5 +* c6) c= (rng c5) \/ (rng c6) ) by FUNCT_4:18, XBOOLE_1:8;
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 E10, 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 E11, 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 M5(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 3;
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 3;
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 JORDAN1:1;
( 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 JORDAN1:1;
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 3;
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;
[#] I[01] = the carrier of I[01] ;
then ( 0 in dom c4 & 1 in dom c4 ) by E7, BORSUK_1:83, TOPS_2:51;
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;

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