:: BORSUK_6 semantic presentation

scheme :: BORSUK_6:sch 1
s1{ F1() -> non empty set , P1[ set ], P2[ set ], P3[ set ], F2( set ) -> set , F3( set ) -> set , F4( set ) -> set } :
ex b1 being Function st
( dom b1 = F1() & ( for b2 being Element of F1() holds
( ( P1[b2] implies b1 . b2 = F2(b2) ) & ( P2[b2] implies b1 . b2 = F3(b2) ) & ( P3[b2] implies b1 . b2 = F4(b2) ) ) ) )
provided
E1: for b1 being Element of F1() holds
( ( P1[b1] implies not P2[b1] ) & ( P1[b1] implies not P3[b1] ) & ( P2[b1] implies not P3[b1] ) ) and
E2: for b1 being Element of F1() holds
( P1[b1] or P2[b1] or P3[b1] )
proof end;

registration
let c1 be Nat;
cluster TOP-REAL a1 -> constituted-FinSeqs ;
coherence
TOP-REAL c1 is constituted-FinSeqs
proof end;
end;

theorem Th1: :: BORSUK_6:1
the carrier of [:I[01] ,I[01] :] = [:[.0,1.],[.0,1.]:] by BORSUK_1:83, BORSUK_1:def 5;

Lemma2: for b1, b2, b3, b4 being complex number holds (((b4 - b3) / b2) * b1) + b3 = ((1 - (b1 / b2)) * b3) + ((b1 / b2) * b4)
by XCMPLX_1:236;

theorem Th2: :: BORSUK_6:2
canceled;

theorem Th3: :: BORSUK_6:3
canceled;

theorem Th4: :: BORSUK_6:4
canceled;

theorem Th5: :: BORSUK_6:5
for b1, b2, b3 being real number st b1 <= b3 & b3 <= b2 holds
(b3 - b1) / (b2 - b1) in the carrier of (Closed-Interval-TSpace 0,1)
proof end;

theorem Th6: :: BORSUK_6:6
for b1 being Point of I[01] st b1 <= 1 / 2 holds
2 * b1 is Point of I[01]
proof end;

theorem Th7: :: BORSUK_6:7
for b1 being Point of I[01] st b1 >= 1 / 2 holds
(2 * b1) - 1 is Point of I[01]
proof end;

theorem Th8: :: BORSUK_6:8
for b1, b2 being Point of I[01] holds b1 * b2 is Point of I[01]
proof end;

theorem Th9: :: BORSUK_6:9
for b1 being Point of I[01] holds (1 / 2) * b1 is Point of I[01]
proof end;

theorem Th10: :: BORSUK_6:10
for b1 being Point of I[01] st b1 >= 1 / 2 holds
b1 - (1 / 4) is Point of I[01]
proof end;

theorem Th11: :: BORSUK_6:11
canceled;

theorem Th12: :: BORSUK_6:12
id I[01] is Path of 0[01] , 1[01]
proof end;

theorem Th13: :: BORSUK_6:13
for b1, b2, b3, b4 being Point of I[01] st b1 <= b2 & b3 <= b4 holds
[:[.b1,b2.],[.b3,b4.]:] is non empty compact Subset of [:I[01] ,I[01] :]
proof end;

theorem Th14: :: BORSUK_6:14
for b1, b2 being Subset of (TOP-REAL 2) st b1 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 <= (2 * (b3 `1 )) - 1 } & b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 <= b3 `1 } holds
(AffineMap 1,0,(1 / 2),(1 / 2)) .: b1 = b2
proof end;

theorem Th15: :: BORSUK_6:15
for b1, b2 being Subset of (TOP-REAL 2) st b1 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 >= (2 * (b3 `1 )) - 1 } & b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 >= b3 `1 } holds
(AffineMap 1,0,(1 / 2),(1 / 2)) .: b1 = b2
proof end;

theorem Th16: :: BORSUK_6:16
for b1, b2 being Subset of (TOP-REAL 2) st b1 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 >= 1 - (2 * (b3 `1 )) } & b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 >= - (b3 `1 ) } holds
(AffineMap 1,0,(1 / 2),(- (1 / 2))) .: b1 = b2
proof end;

theorem Th17: :: BORSUK_6:17
for b1, b2 being Subset of (TOP-REAL 2) st b1 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 <= 1 - (2 * (b3 `1 )) } & b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 <= - (b3 `1 ) } holds
(AffineMap 1,0,(1 / 2),(- (1 / 2))) .: b1 = b2
proof end;

definition
let c1 be 1-sorted ;
attr a1 is real-membered means :Def1: :: BORSUK_6:def 1
the carrier of a1 is real-membered;
end;

:: deftheorem Def1 defines real-membered BORSUK_6:def 1 :
for b1 being 1-sorted holds
( b1 is real-membered iff the carrier of b1 is real-membered );

theorem Th18: :: BORSUK_6:18
for b1 being non empty 1-sorted holds
( b1 is real-membered iff for b2 being Element of b1 holds b2 is real )
proof end;

registration
cluster I[01] -> real-membered ;
coherence
I[01] is real-membered
proof end;
end;

registration
cluster non empty real-membered 1-sorted ;
existence
ex b1 being 1-sorted st
( not b1 is empty & b1 is real-membered )
proof end;
cluster non empty real-membered TopStruct ;
existence
ex b1 being TopSpace st
( not b1 is empty & b1 is real-membered )
proof end;
end;

registration
let c1 be real-membered 1-sorted ;
cluster -> real Element of the carrier of a1;
coherence
for b1 being Element of c1 holds b1 is real
proof end;
end;

registration
let c1 be real-membered TopStruct ;
cluster -> real-membered SubSpace of a1;
coherence
for b1 being SubSpace of c1 holds b1 is real-membered
proof end;
end;

registration
let c1, c2 be non empty real-membered TopSpace;
let c3 be Element of [:c1,c2:];
cluster a3 `1 -> real ;
coherence
c3 `1 is real
proof end;
cluster a3 `2 -> real ;
coherence
c3 `2 is real
proof end;
end;

registration
let c1 be non empty SubSpace of [:I[01] ,I[01] :];
let c2 be Point of c1;
cluster a2 `1 -> real ;
coherence
c2 `1 is real
proof end;
cluster a2 `2 -> real ;
coherence
c2 `2 is real
proof end;
end;

registration
cluster R^1 -> real-membered ;
coherence
R^1 is real-membered
proof end;
end;

theorem Th19: :: BORSUK_6:19
{ b1 where B is Point of (TOP-REAL 2) : b1 `2 <= (2 * (b1 `1 )) - 1 } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th20: :: BORSUK_6:20
{ b1 where B is Point of (TOP-REAL 2) : b1 `2 >= (2 * (b1 `1 )) - 1 } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th21: :: BORSUK_6:21
{ b1 where B is Point of (TOP-REAL 2) : b1 `2 <= 1 - (2 * (b1 `1 )) } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th22: :: BORSUK_6:22
{ b1 where B is Point of (TOP-REAL 2) : b1 `2 >= 1 - (2 * (b1 `1 )) } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th23: :: BORSUK_6:23
{ b1 where B is Point of (TOP-REAL 2) : ( b1 `2 >= 1 - (2 * (b1 `1 )) & b1 `2 >= (2 * (b1 `1 )) - 1 ) } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th24: :: BORSUK_6:24
ex b1 being Function of [:R^1 ,R^1 :],(TOP-REAL 2) st
for b2, b3 being Real holds b1 . [b2,b3] = <*b2,b3*>
proof end;

theorem Th25: :: BORSUK_6:25
{ b1 where B is Point of [:R^1 ,R^1 :] : b1 `2 <= 1 - (2 * (b1 `1 )) } is closed Subset of [:R^1 ,R^1 :]
proof end;

theorem Th26: :: BORSUK_6:26
{ b1 where B is Point of [:R^1 ,R^1 :] : b1 `2 <= (2 * (b1 `1 )) - 1 } is closed Subset of [:R^1 ,R^1 :]
proof end;

theorem Th27: :: BORSUK_6:27
{ b1 where B is Point of [:R^1 ,R^1 :] : ( b1 `2 >= 1 - (2 * (b1 `1 )) & b1 `2 >= (2 * (b1 `1 )) - 1 ) } is closed Subset of [:R^1 ,R^1 :]
proof end;

theorem Th28: :: BORSUK_6:28
{ b1 where B is Point of [:I[01] ,I[01] :] : b1 `2 <= 1 - (2 * (b1 `1 )) } is non empty closed Subset of [:I[01] ,I[01] :]
proof end;

theorem Th29: :: BORSUK_6:29
{ b1 where B is Point of [:I[01] ,I[01] :] : ( b1 `2 >= 1 - (2 * (b1 `1 )) & b1 `2 >= (2 * (b1 `1 )) - 1 ) } is non empty closed Subset of [:I[01] ,I[01] :]
proof end;

theorem Th30: :: BORSUK_6:30
{ b1 where B is Point of [:I[01] ,I[01] :] : b1 `2 <= (2 * (b1 `1 )) - 1 } is non empty closed Subset of [:I[01] ,I[01] :]
proof end;

theorem Th31: :: BORSUK_6:31
for b1, b2 being non empty TopSpace
for b3 being Point of [:b1,b2:] holds
( b3 `1 is Point of b1 & b3 `2 is Point of b2 )
proof end;

theorem Th32: :: BORSUK_6:32
for b1, b2 being Subset of [:I[01] ,I[01] :] st b1 = [:[.0,(1 / 2).],[.0,1.]:] & b2 = [:[.(1 / 2),1.],[.0,1.]:] holds
([#] ([:I[01] ,I[01] :] | b1)) \/ ([#] ([:I[01] ,I[01] :] | b2)) = [#] [:I[01] ,I[01] :]
proof end;

theorem Th33: :: BORSUK_6:33
for b1, b2 being Subset of [:I[01] ,I[01] :] st b1 = [:[.0,(1 / 2).],[.0,1.]:] & b2 = [:[.(1 / 2),1.],[.0,1.]:] holds
([#] ([:I[01] ,I[01] :] | b1)) /\ ([#] ([:I[01] ,I[01] :] | b2)) = [:{(1 / 2)},[.0,1.]:]
proof end;

registration
let c1 be TopStruct ;
cluster {} a1 -> compact ;
coherence
{} c1 is compact by COMPTS_1:9;
end;

registration
let c1 be TopStruct ;
cluster empty compact Element of bool the carrier of a1;
existence
ex b1 being Subset of c1 st
( b1 is empty & b1 is compact )
proof end;
end;

theorem Th34: :: BORSUK_6:34
for b1 being TopStruct holds {} is empty compact Subset of b1
proof end;

theorem Th35: :: BORSUK_6:35
for b1 being TopStruct
for b2, b3 being real number st b2 > b3 holds
[.b2,b3.] is empty compact Subset of b1
proof end;

theorem Th36: :: BORSUK_6:36
for b1, b2, b3, b4 being Point of I[01] holds [:[.b1,b2.],[.b3,b4.]:] is compact Subset of [:I[01] ,I[01] :]
proof end;

definition
let c1, c2, c3, c4 be real number ;
func L[01] c1,c2,c3,c4 -> Function of (Closed-Interval-TSpace a1,a2),(Closed-Interval-TSpace a3,a4) equals :: BORSUK_6:def 2
(L[01] ((#) a3,a4),(a3,a4 (#) )) * (P[01] a1,a2,((#) 0,1),(0,1 (#) ));
correctness
coherence
(L[01] ((#) c3,c4),(c3,c4 (#) )) * (P[01] c1,c2,((#) 0,1),(0,1 (#) )) is Function of (Closed-Interval-TSpace c1,c2),(Closed-Interval-TSpace c3,c4);
;
end;

:: deftheorem Def2 defines L[01] BORSUK_6:def 2 :
for b1, b2, b3, b4 being real number holds L[01] b1,b2,b3,b4 = (L[01] ((#) b3,b4),(b3,b4 (#) )) * (P[01] b1,b2,((#) 0,1),(0,1 (#) ));

theorem Th37: :: BORSUK_6:37
for b1, b2, b3, b4 being real number st b1 < b2 & b3 < b4 holds
( (L[01] b1,b2,b3,b4) . b1 = b3 & (L[01] b1,b2,b3,b4) . b2 = b4 )
proof end;

theorem Th38: :: BORSUK_6:38
for b1, b2, b3, b4 being real number st b1 < b2 & b3 <= b4 holds
L[01] b1,b2,b3,b4 is continuous Function of (Closed-Interval-TSpace b1,b2),(Closed-Interval-TSpace b3,b4)
proof end;

theorem Th39: :: BORSUK_6:39
for b1, b2, b3, b4 being real number st b1 < b2 & b3 <= b4 holds
for b5 being real number st b1 <= b5 & b5 <= b2 holds
(L[01] b1,b2,b3,b4) . b5 = (((b4 - b3) / (b2 - b1)) * (b5 - b1)) + b3
proof end;

theorem Th40: :: BORSUK_6:40
for b1, b2 being Function of [:I[01] ,I[01] :],I[01] st b1 is continuous & b2 is continuous & ( for b3 being Point of [:I[01] ,I[01] :] holds (b1 . b3) * (b2 . b3) is Point of I[01] ) holds
ex b3 being Function of [:I[01] ,I[01] :],I[01] st
( ( for b4 being Point of [:I[01] ,I[01] :]
for b5, b6 being real number st b1 . b4 = b5 & b2 . b4 = b6 holds
b3 . b4 = b5 * b6 ) & b3 is continuous )
proof end;

theorem Th41: :: BORSUK_6:41
for b1, b2 being Function of [:I[01] ,I[01] :],I[01] st b1 is continuous & b2 is continuous & ( for b3 being Point of [:I[01] ,I[01] :] holds (b1 . b3) + (b2 . b3) is Point of I[01] ) holds
ex b3 being Function of [:I[01] ,I[01] :],I[01] st
( ( for b4 being Point of [:I[01] ,I[01] :]
for b5, b6 being real number st b1 . b4 = b5 & b2 . b4 = b6 holds
b3 . b4 = b5 + b6 ) & b3 is continuous )
proof end;

theorem Th42: :: BORSUK_6:42
for b1, b2 being Function of [:I[01] ,I[01] :],I[01] st b1 is continuous & b2 is continuous & ( for b3 being Point of [:I[01] ,I[01] :] holds (b1 . b3) - (b2 . b3) is Point of I[01] ) holds
ex b3 being Function of [:I[01] ,I[01] :],I[01] st
( ( for b4 being Point of [:I[01] ,I[01] :]
for b5, b6 being real number st b1 . b4 = b5 & b2 . b4 = b6 holds
b3 . b4 = b5 - b6 ) & b3 is continuous )
proof end;

theorem Th43: :: BORSUK_6:43
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3 st b4 is continuous holds
b4 * (L[01] (0,1 (#) ),((#) 0,1)) is continuous Function of I[01] ,b1
proof end;

theorem Th44: :: BORSUK_6:44
for b1 being non empty TopStruct
for b2, b3 being Point of b1
for b4 being Path of b2,b3 st b4 . 0 = b2 & b4 . 1 = b3 holds
( (b4 * (L[01] (0,1 (#) ),((#) 0,1))) . 0 = b3 & (b4 * (L[01] (0,1 (#) ),((#) 0,1))) . 1 = b2 )
proof end;

theorem Th45: :: BORSUK_6:45
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3 st b4 is continuous & b4 . 0 = b2 & b4 . 1 = b3 holds
( - b4 is continuous & (- b4) . 0 = b3 & (- b4) . 1 = b2 )
proof end;

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 end;
symmetry
for b1, b2 being Point of c1 st b1,b2 are_connected holds
b2,b1 are_connected
proof end;
end;

theorem Th46: :: BORSUK_6:46
for b1 being non empty TopSpace
for b2, b3, b4 being Point of b1 st b2,b3 are_connected & b3,b4 are_connected holds
b2,b4 are_connected
proof end;

theorem Th47: :: BORSUK_6:47
canceled;

theorem Th48: :: BORSUK_6:48
canceled;

theorem Th49: :: BORSUK_6:49
canceled;

theorem Th50: :: BORSUK_6:50
for b1 being non empty TopSpace
for b2, b3 being Point of b1 st b2,b3 are_connected holds
for b4 being Path of b2,b3 holds b4 = - (- b4)
proof end;

theorem Th51: :: BORSUK_6:51
for b1 being non empty arcwise_connected TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3 holds b4 = - (- b4)
proof end;

definition
let c1 be non empty arcwise_connected TopSpace;
let c2, c3, c4 be Point of c1;
let c5 be Path of c2,c3;
let c6 be Path of c3,c4;
canceled;
redefine func c5 + c6 -> Path of a2,a4 means :: BORSUK_6:def 4
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) ) );
compatibility
for b1 being Path of c2,c4 holds
( b1 = c5 + c6 iff 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 end;
end;

:: deftheorem Def3 BORSUK_6:def 3 :
canceled;

:: deftheorem Def4 defines + BORSUK_6:def 4 :
for b1 being non empty arcwise_connected TopSpace
for b2, b3, b4 being Point of b1
for b5 being Path of b2,b3
for b6 being Path of b3,b4
for b7 being Path of b2,b4 holds
( b7 = b5 + b6 iff for b8 being Point of I[01] holds
( ( b8 <= 1 / 2 implies b7 . b8 = b5 . (2 * b8) ) & ( 1 / 2 <= b8 implies b7 . b8 = b6 . ((2 * b8) - 1) ) ) );

definition
let c1 be non empty arcwise_connected TopSpace;
let c2, c3 be Point of c1;
let c4 be Path of c2,c3;
redefine func - c4 -> Path of a3,a2 means :Def5: :: BORSUK_6:def 5
for b1 being Point of I[01] holds a5 . b1 = a4 . (1 - b1);
compatibility
for b1 being Path of c3,c2 holds
( b1 = - c4 iff for b2 being Point of I[01] holds b1 . b2 = c4 . (1 - b2) )
proof end;
end;

:: deftheorem Def5 defines - BORSUK_6:def 5 :
for b1 being non empty arcwise_connected TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being Path of b3,b2 holds
( b5 = - b4 iff for b6 being Point of I[01] holds b5 . b6 = b4 . (1 - b6) );

definition
let c1 be non empty TopSpace;
let c2, c3 be Point of c1;
let c4 be Path of c2,c3;
let c5 be continuous Function of I[01] ,I[01] ;
assume E45: ( c5 . 0 = 0 & c5 . 1 = 1 & c2,c3 are_connected ) ;
func RePar c4,c5 -> Path of a2,a3 equals :Def6: :: BORSUK_6:def 6
a4 * a5;
coherence
c4 * c5 is Path of c2,c3
proof end;
end;

:: deftheorem Def6 defines RePar BORSUK_6:def 6 :
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being continuous Function of I[01] ,I[01] st b5 . 0 = 0 & b5 . 1 = 1 & b2,b3 are_connected holds
RePar b4,b5 = b4 * b5;

theorem Th52: :: BORSUK_6:52
canceled;

theorem Th53: :: BORSUK_6:53
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being continuous Function of I[01] ,I[01] st b5 . 0 = 0 & b5 . 1 = 1 & b2,b3 are_connected holds
RePar b4,b5,b4 are_homotopic
proof end;

theorem Th54: :: BORSUK_6:54
for b1 being non empty arcwise_connected TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being continuous Function of I[01] ,I[01] st b5 . 0 = 0 & b5 . 1 = 1 holds
RePar b4,b5,b4 are_homotopic
proof end;

definition
func 1RP -> Function of I[01] ,I[01] means :Def7: :: BORSUK_6:def 7
for b1 being Point of I[01] holds
( ( b1 <= 1 / 2 implies a1 . b1 = 2 * b1 ) & ( b1 > 1 / 2 implies a1 . b1 = 1 ) );
existence
ex b1 being Function of I[01] ,I[01] st
for b2 being Point of I[01] holds
( ( b2 <= 1 / 2 implies b1 . b2 = 2 * b2 ) & ( b2 > 1 / 2 implies b1 . b2 = 1 ) )
proof end;
uniqueness
for b1, b2 being Function of I[01] ,I[01] st ( for b3 being Point of I[01] holds
( ( b3 <= 1 / 2 implies b1 . b3 = 2 * b3 ) & ( b3 > 1 / 2 implies b1 . b3 = 1 ) ) ) & ( for b3 being Point of I[01] holds
( ( b3 <= 1 / 2 implies b2 . b3 = 2 * b3 ) & ( b3 > 1 / 2 implies b2 . b3 = 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines 1RP BORSUK_6:def 7 :
for b1 being Function of I[01] ,I[01] holds
( b1 = 1RP iff for b2 being Point of I[01] holds
( ( b2 <= 1 / 2 implies b1 . b2 = 2 * b2 ) & ( b2 > 1 / 2 implies b1 . b2 = 1 ) ) );

registration
cluster 1RP -> continuous ;
coherence
1RP is continuous
proof end;
end;

theorem Th55: :: BORSUK_6:55
( 1RP . 0 = 0 & 1RP . 1 = 1 )
proof end;

definition
func 2RP -> Function of I[01] ,I[01] means :Def8: :: BORSUK_6:def 8
for b1 being Point of I[01] holds
( ( b1 <= 1 / 2 implies a1 . b1 = 0 ) & ( b1 > 1 / 2 implies a1 . b1 = (2 * b1) - 1 ) );
existence
ex b1 being Function of I[01] ,I[01] st
for b2 being Point of I[01] holds
( ( b2 <= 1 / 2 implies b1 . b2 = 0 ) & ( b2 > 1 / 2 implies b1 . b2 = (2 * b2) - 1 ) )
proof end;
uniqueness
for b1, b2 being Function of I[01] ,I[01] st ( for b3 being Point of I[01] holds
( ( b3 <= 1 / 2 implies b1 . b3 = 0 ) & ( b3 > 1 / 2 implies b1 . b3 = (2 * b3) - 1 ) ) ) & ( for b3 being Point of I[01] holds
( ( b3 <= 1 / 2 implies b2 . b3 = 0 ) & ( b3 > 1 / 2 implies b2 . b3 = (2 * b3) - 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines 2RP BORSUK_6:def 8 :
for b1 being Function of I[01] ,I[01] holds
( b1 = 2RP iff for b2 being Point of I[01] holds
( ( b2 <= 1 / 2 implies b1 . b2 = 0 ) & ( b2 > 1 / 2 implies b1 . b2 = (2 * b2) - 1 ) ) );

registration
cluster 2RP -> continuous ;
coherence
2RP is continuous
proof end;
end;

theorem Th56: :: BORSUK_6:56
( 2RP . 0 = 0 & 2RP . 1 = 1 )
proof end;

definition
func 3RP -> Function of I[01] ,I[01] means :Def9: :: BORSUK_6:def 9
for b1 being Point of I[01] holds
( ( b1 <= 1 / 2 implies a1 . b1 = (1 / 2) * b1 ) & ( b1 > 1 / 2 & b1 <= 3 / 4 implies a1 . b1 = b1 - (1 / 4) ) & ( b1 > 3 / 4 implies a1 . b1 = (2 * b1) - 1 ) );
existence
ex b1 being Function of I[01] ,I[01] st
for b2 being Point of I[01] holds
( ( b2 <= 1 / 2 implies b1 . b2 = (1 / 2) * b2 ) & ( b2 > 1 / 2 & b2 <= 3 / 4 implies b1 . b2 = b2 - (1 / 4) ) & ( b2 > 3 / 4 implies b1 . b2 = (2 * b2) - 1 ) )
proof end;
uniqueness
for b1, b2 being Function of I[01] ,I[01] st ( for b3 being Point of I[01] holds
( ( b3 <= 1 / 2 implies b1 . b3 = (1 / 2) * b3 ) & ( b3 > 1 / 2 & b3 <= 3 / 4 implies b1 . b3 = b3 - (1 / 4) ) & ( b3 > 3 / 4 implies b1 . b3 = (2 * b3) - 1 ) ) ) & ( for b3 being Point of I[01] holds
( ( b3 <= 1 / 2 implies b2 . b3 = (1 / 2) * b3 ) & ( b3 > 1 / 2 & b3 <= 3 / 4 implies b2 . b3 = b3 - (1 / 4) ) & ( b3 > 3 / 4 implies b2 . b3 = (2 * b3) - 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines 3RP BORSUK_6:def 9 :
for b1 being Function of I[01] ,I[01] holds
( b1 = 3RP iff for b2 being Point of I[01] holds
( ( b2 <= 1 / 2 implies b1 . b2 = (1 / 2) * b2 ) & ( b2 > 1 / 2 & b2 <= 3 / 4 implies b1 . b2 = b2 - (1 / 4) ) & ( b2 > 3 / 4 implies b1 . b2 = (2 * b2) - 1 ) ) );

registration
cluster 3RP -> continuous ;
coherence
3RP is continuous
proof end;
end;

theorem Th57: :: BORSUK_6:57
( 3RP . 0 = 0 & 3RP . 1 = 1 )
proof end;

theorem Th58: :: BORSUK_6:58
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being constant Path of b3,b3 st b2,b3 are_connected holds
RePar b4,1RP = b4 + b5
proof end;

theorem Th59: :: BORSUK_6:59
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being constant Path of b2,b2 st b2,b3 are_connected holds
RePar b4,2RP = b5 + b4
proof end;

theorem Th60: :: BORSUK_6:60
for b1 being non empty TopSpace
for b2, b3, b4, b5 being Point of b1
for b6 being Path of b2,b3
for b7 being Path of b3,b4
for b8 being Path of b4,b5 st b2,b3 are_connected & b3,b4 are_connected & b4,b5 are_connected holds
RePar ((b6 + b7) + b8),3RP = b6 + (b7 + b8)
proof end;

definition
func LowerLeftUnitTriangle -> Subset of [:I[01] ,I[01] :] means :Def10: :: BORSUK_6:def 10
for b1 being set holds
( b1 in a1 iff ex b2, b3 being Point of I[01] st
( b1 = [b2,b3] & b3 <= 1 - (2 * b2) ) );
existence
ex b1 being Subset of [:I[01] ,I[01] :] st
for b2 being set holds
( b2 in b1 iff ex b3, b4 being Point of I[01] st
( b2 = [b3,b4] & b4 <= 1 - (2 * b3) ) )
proof end;
uniqueness
for b1, b2 being Subset of [:I[01] ,I[01] :] st ( for b3 being set holds
( b3 in b1 iff ex b4, b5 being Point of I[01] st
( b3 = [b4,b5] & b5 <= 1 - (2 * b4) ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4, b5 being Point of I[01] st
( b3 = [b4,b5] & b5 <= 1 - (2 * b4) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines LowerLeftUnitTriangle BORSUK_6:def 10 :
for b1 being Subset of [:I[01] ,I[01] :] holds
( b1 = LowerLeftUnitTriangle iff for b2 being set holds
( b2 in b1 iff ex b3, b4 being Point of I[01] st
( b2 = [b3,b4] & b4 <= 1 - (2 * b3) ) ) );

notation
synonym IAA for LowerLeftUnitTriangle ;
end;

definition
func UpperUnitTriangle -> Subset of [:I[01] ,I[01] :] means :Def11: :: BORSUK_6:def 11
for b1 being set holds
( b1 in a1 iff ex b2, b3 being Point of I[01] st
( b1 = [b2,b3] & b3 >= 1 - (2 * b2) & b3 >= (2 * b2) - 1 ) );
existence
ex b1 being Subset of [:I[01] ,I[01] :] st
for b2 being set holds
( b2 in b1 iff ex b3, b4 being Point of I[01] st
( b2 = [b3,b4] & b4 >= 1 - (2 * b3) & b4 >= (2 * b3) - 1 ) )
proof end;
uniqueness
for b1, b2 being Subset of [:I[01] ,I[01] :] st ( for b3 being set holds
( b3 in b1 iff ex b4, b5 being Point of I[01] st
( b3 = [b4,b5] & b5 >= 1 - (2 * b4) & b5 >= (2 * b4) - 1 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4, b5 being Point of I[01] st
( b3 = [b4,b5] & b5 >= 1 - (2 * b4) & b5 >= (2 * b4) - 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines UpperUnitTriangle BORSUK_6:def 11 :
for b1 being Subset of [:I[01] ,I[01] :] holds
( b1 = UpperUnitTriangle iff for b2 being set holds
( b2 in b1 iff ex b3, b4 being Point of I[01] st
( b2 = [b3,b4] & b4 >= 1 - (2 * b3) & b4 >= (2 * b3) - 1 ) ) );

notation
synonym IBB for UpperUnitTriangle ;
end;

definition
func LowerRightUnitTriangle -> Subset of [:I[01] ,I[01] :] means :Def12: :: BORSUK_6:def 12
for b1 being set holds
( b1 in a1 iff ex b2, b3 being Point of I[01] st
( b1 = [b2,b3] & b3 <= (2 * b2) - 1 ) );
existence
ex b1 being Subset of [:I[01] ,I[01] :] st
for b2 being set holds
( b2 in b1 iff ex b3, b4 being Point of I[01] st
( b2 = [b3,b4] & b4 <= (2 * b3) - 1 ) )
proof end;
uniqueness
for b1, b2 being Subset of [:I[01] ,I[01] :] st ( for b3 being set holds
( b3 in b1 iff ex b4, b5 being Point of I[01] st
( b3 = [b4,b5] & b5 <= (2 * b4) - 1 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4, b5 being Point of I[01] st
( b3 = [b4,b5] & b5 <= (2 * b4) - 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines LowerRightUnitTriangle BORSUK_6:def 12 :
for b1 being Subset of [:I[01] ,I[01] :] holds
( b1 = LowerRightUnitTriangle iff for b2 being set holds
( b2 in b1 iff ex b3, b4 being Point of I[01] st
( b2 = [b3,b4] & b4 <= (2 * b3) - 1 ) ) );

notation
synonym ICC for LowerRightUnitTriangle ;
end;

theorem Th61: :: BORSUK_6:61
IAA = { b1 where B is Point of [:I[01] ,I[01] :] : b1 `2 <= 1 - (2 * (b1 `1 )) }
proof end;

theorem Th62: :: BORSUK_6:62
IBB = { b1 where B is Point of [:I[01] ,I[01] :] : ( b1 `2 >= 1 - (2 * (b1 `1 )) & b1 `2 >= (2 * (b1 `1 )) - 1 ) }
proof end;

theorem Th63: :: BORSUK_6:63
ICC = { b1 where B is Point of [:I[01] ,I[01] :] : b1 `2 <= (2 * (b1 `1 )) - 1 }
proof end;

registration
cluster LowerLeftUnitTriangle -> non empty closed ;
coherence
( IAA is closed & not IAA is empty ) by Th28, Th61;
cluster UpperUnitTriangle -> non empty closed ;
coherence
( IBB is closed & not IBB is empty ) by Th29, Th62;
cluster LowerRightUnitTriangle -> non empty closed ;
coherence
( ICC is closed & not ICC is empty ) by Th30, Th63;
end;

theorem Th64: :: BORSUK_6:64
(IAA \/ IBB ) \/ ICC = [:[.0,1.],[.0,1.]:]
proof end;

theorem Th65: :: BORSUK_6:65
IAA /\ IBB = { b1 where B is Point of [:I[01] ,I[01] :] : b1 `2 = 1 - (2 * (b1 `1 )) }
proof end;

theorem Th66: :: BORSUK_6:66
ICC /\ IBB = { b1 where B is Point of [:I[01] ,I[01] :] : b1 `2 = (2 * (b1 `1 )) - 1 }
proof end;

theorem Th67: :: BORSUK_6:67
for b1 being Point of [:I[01] ,I[01] :] st b1 in IAA holds
b1 `1 <= 1 / 2
proof end;

theorem Th68: :: BORSUK_6:68
for b1 being Point of [:I[01] ,I[01] :] st b1 in ICC holds
b1 `1 >= 1 / 2
proof end;

theorem Th69: :: BORSUK_6:69
for b1 being Point of I[01] holds [0,b1] in IAA
proof end;

theorem Th70: :: BORSUK_6:70
for b1 being set st [0,b1] in IBB holds
b1 = 1
proof end;

theorem Th71: :: BORSUK_6:71
for b1 being set st [b1,1] in ICC holds
b1 = 1
proof end;

theorem Th72: :: BORSUK_6:72
[0,1] in IBB
proof end;

theorem Th73: :: BORSUK_6:73
for b1 being Point of I[01] holds [b1,1] in IBB
proof end;

theorem Th74: :: BORSUK_6:74
( [(1 / 2),0] in ICC & [1,1] in ICC )
proof end;

theorem Th75: :: BORSUK_6:75
[(1 / 2),0] in IBB
proof end;

theorem Th76: :: BORSUK_6:76
for b1 being Point of I[01] holds [1,b1] in ICC
proof end;

theorem Th77: :: BORSUK_6:77
for b1 being Point of I[01] st b1 >= 1 / 2 holds
[b1,0] in ICC
proof end;

theorem Th78: :: BORSUK_6:78
for b1 being Point of I[01] st b1 <= 1 / 2 holds
[b1,0] in IAA
proof end;

theorem Th79: :: BORSUK_6:79
for b1 being Point of I[01] st b1 < 1 / 2 holds
( not [b1,0] in IBB & not [b1,0] in ICC )
proof end;

theorem Th80: :: BORSUK_6:80
IAA /\ ICC = {[(1 / 2),0]}
proof end;

Lemma79: for b1, b2 being Point of I[01] holds [b1,b2] in the carrier of [:I[01] ,I[01] :]
;

theorem Th81: :: BORSUK_6:81
for b1 being non empty TopSpace
for b2, b3, b4, b5 being Point of b1
for b6 being Path of b2,b3
for b7 being Path of b3,b4
for b8 being Path of b4,b5 st b2,b3 are_connected & b3,b4 are_connected & b4,b5 are_connected holds
(b6 + b7) + b8,b6 + (b7 + b8) are_homotopic
proof end;

theorem Th82: :: BORSUK_6:82
for b1 being non empty arcwise_connected TopSpace
for b2, b3, b4, b5 being Point of b1
for b6 being Path of b2,b3
for b7 being Path of b3,b4
for b8 being Path of b4,b5 holds (b6 + b7) + b8,b6 + (b7 + b8) are_homotopic
proof end;

theorem Th83: :: BORSUK_6:83
for b1 being non empty TopSpace
for b2, b3, b4 being Point of b1
for b5, b6 being Path of b2,b3
for b7, b8 being Path of b3,b4 st b2,b3 are_connected & b3,b4 are_connected & b5,b6 are_homotopic & b7,b8 are_homotopic holds
b5 + b7,b6 + b8 are_homotopic
proof end;

theorem Th84: :: BORSUK_6:84
for b1 being non empty arcwise_connected TopSpace
for b2, b3, b4 being Point of b1
for b5, b6 being Path of b2,b3
for b7, b8 being Path of b3,b4 st b5,b6 are_homotopic & b7,b8 are_homotopic holds
b5 + b7,b6 + b8 are_homotopic
proof end;

theorem Th85: :: BORSUK_6:85
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4, b5 being Path of b2,b3 st b2,b3 are_connected & b4,b5 are_homotopic holds
- b4, - b5 are_homotopic
proof end;

theorem Th86: :: BORSUK_6:86
for b1 being non empty arcwise_connected TopSpace
for b2, b3 being Point of b1
for b4, b5 being Path of b2,b3 st b4,b5 are_homotopic holds
- b4, - b5 are_homotopic
proof end;

theorem Th87: :: BORSUK_6:87
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4, b5, b6 being Path of b2,b3 st b4,b5 are_homotopic & b5,b6 are_homotopic holds
b4,b6 are_homotopic
proof end;

theorem Th88: :: BORSUK_6:88
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being constant Path of b3,b3 st b2,b3 are_connected holds
b4 + b5,b4 are_homotopic
proof end;

theorem Th89: :: BORSUK_6:89
for b1 being non empty arcwise_connected TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being constant Path of b3,b3 holds b4 + b5,b4 are_homotopic
proof end;

theorem Th90: :: BORSUK_6:90
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being constant Path of b2,b2 st b2,b3 are_connected holds
b5 + b4,b4 are_homotopic
proof end;

theorem Th91: :: BORSUK_6:91
for b1 being non empty arcwise_connected TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being constant Path of b2,b2 holds b5 + b4,b4 are_homotopic
proof end;

theorem Th92: :: BORSUK_6:92
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being constant Path of b2,b2 st b2,b3 are_connected holds
b4 + (- b4),b5 are_homotopic
proof end;

theorem Th93: :: BORSUK_6:93
for b1 being non empty arcwise_connected TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being constant Path of b2,b2 holds b4 + (- b4),b5 are_homotopic
proof end;

theorem Th94: :: BORSUK_6:94
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being constant Path of b3,b3 st b2,b3 are_connected holds
(- b4) + b4,b5 are_homotopic
proof end;

theorem Th95: :: BORSUK_6:95
for b1 being non empty arcwise_connected TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3
for b5 being constant Path of b3,b3 holds (- b4) + b4,b5 are_homotopic
proof end;

theorem Th96: :: BORSUK_6:96
for b1 being non empty TopSpace
for b2 being Point of b1
for b3, b4 being constant Path of b2,b2 holds b3,b4 are_homotopic
proof end;

definition
let c1 be non empty TopSpace;
let c2, c3 be Point of c1;
let c4, c5 be Path of c2,c3;
assume E87: c4,c5 are_homotopic ;
mode Homotopy of c4,c5 -> Function of [:I[01] ,I[01] :],a1 means :: BORSUK_6:def 13
( a6 is continuous & ( for b1 being Point of I[01] holds
( a6 . b1,0 = a4 . b1 & a6 . b1,1 = a5 . b1 & ( for b2 being Point of I[01] holds
( a6 . 0,b2 = a2 & a6 . 1,b2 = a3 ) ) ) ) );
existence
ex b1 being Function of [:I[01] ,I[01] :],c1 st
( b1 is continuous & ( for b2 being Point of I[01] holds
( b1 . b2,0 = c4 . b2 & b1 . b2,1 = c5 . b2 & ( for b3 being Point of I[01] holds
( b1 . 0,b3 = c2 & b1 . 1,b3 = c3 ) ) ) ) ) by E87, BORSUK_2:def 7;
end;

:: deftheorem Def13 defines Homotopy BORSUK_6:def 13 :
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4, b5 being Path of b2,b3 st b4,b5 are_homotopic holds
for b6 being Function of [:I[01] ,I[01] :],b1 holds
( b6 is Homotopy of b4,b5 iff ( b6 is continuous & ( for b7 being Point of I[01] holds
( b6 . b7,0 = b4 . b7 & b6 . b7,1 = b5 . b7 & ( for b8 being Point of I[01] holds
( b6 . 0,b8 = b2 & b6 . 1,b8 = b3 ) ) ) ) ) );