let T be non empty TopSpace; :: thesis:
let a, b be Point of T; :: thesis:
set X = [:I[01],I[01]:];
reconsider G2 = pr2 ( the carrier of I[01], the carrier of I[01]) as continuous Function of [:I[01],I[01]:],I[01] by YELLOW12:40;
reconsider F2 = pr1 ( the carrier of I[01], the carrier of I[01]) as continuous Function of [:I[01],I[01]:],I[01] by YELLOW12:39;
reconsider f3 = pr1 ( the carrier of I[01], the carrier of I[01]) as continuous Function of [:I[01],I[01]:],I[01] by YELLOW12:39;
reconsider f4 = pr2 ( the carrier of I[01], the carrier of I[01]) as continuous Function of [:I[01],I[01]:],I[01] by YELLOW12:40;
reconsider ID = id I[01] as Path of 0[01] , 1[01] by Th8;
let P be Path of a,b; :: thesis:
let f be continuous Function of I[01],I[01]; :: thesis:
assume that
A1: f . 0 = 0 and
A2: f . 1 = 1 and
A3: a,b are_connected ; :: thesis:
reconsider f2 = f * F2 as continuous Function of [:I[01],I[01]:],I[01] ;
set G1 = - ID;
reconsider f1 = (- ID) * G2 as continuous Function of [:I[01],I[01]:],I[01] ;
A4: for s, t being Point of I[01] holds f1 . [s,t] = 1 - t

proof

let s, t be Point of I[01]; :: thesis:
A5: 1 - t in the carrier of I[01] by JORDAN5B:4;
[s,t] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then [s,t] in dom G2 by FUNCT_2:def 1;
then f1 . [s,t] = (- ID) . (G2 . (s,t)) by FUNCT_1:13
.= (- ID) . t by FUNCT_3:def 5
.= ID . (1 - t) by Def3
.= 1 - t by A5, FUNCT_1:18 ;
hence f1 . [s,t] = 1 - t ; :: thesis:

end;

for p being Point of [:I[01],I[01]:] holds (f3 . p) * (f4 . p) is Point of I[01] by Th5;
then consider g2 being Function of [:I[01],I[01]:],I[01] such that
A6: for p being Point of [:I[01],I[01]:]
for r1, r2 being Real st f3 . p = r1 & f4 . p = r2 holds
g2 . p = r1 * r2 and
A7: g2 is continuous by Th36;
for p being Point of [:I[01],I[01]:] holds (f1 . p) * (f2 . p) is Point of I[01] by Th5;
then consider g1 being Function of [:I[01],I[01]:],I[01] such that
A8: for p being Point of [:I[01],I[01]:]
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g1 . p = r1 * r2 and
A9: g1 is continuous by Th36;
A10: for s, t being Point of I[01] holds f2 . (s,t) = f . s

proof

let s, t be Point of I[01]; :: thesis:
[s,t] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then [s,t] in dom F2 by FUNCT_2:def 1;
hence f2 . (s,t) = f . (F2 . (s,t)) by FUNCT_1:13
.= f . s by FUNCT_3:def 4 ;
:: thesis:

end;

A11: for t, s being Point of I[01] holds g1 . [s,t] = (1 - t) * (f . s)

proof

let t, s be Point of I[01]; :: thesis:
( f1 . (s,t) = 1 - t & f2 . (s,t) = f . s ) by A4, A10;
hence g1 . [s,t] = (1 - t) * (f . s) by A8; :: thesis:

end;

A12: for t, s being Point of I[01] holds g2 . [s,t] = t * s

proof

let t, s be Point of I[01]; :: thesis:
( f3 . (s,t) = s & f4 . (s,t) = t ) by FUNCT_3:def 4, FUNCT_3:def 5;
hence g2 . [s,t] = t * s by A6; :: thesis:

end;

for p being Point of [:I[01],I[01]:] holds (g1 . p) + (g2 . p) is Point of I[01]

proof

let p be Point of [:I[01],I[01]:]; :: thesis:
p in the carrier of [:I[01],I[01]:] ;
then p in [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then consider s, t being object such that
A13: ( s in the carrier of I[01] & t in the carrier of I[01] ) and
A14: p = [s,t] by ZFMISC_1:def 2;
reconsider s = s, t = t as Point of I[01] by A13;
set a = f . s;

per cases ;

suppose A15: f . s <= s ; :: thesis:

A16: s <= 1 by BORSUK_1:40, XXREAL_1:1;
A17: t <= 1 by BORSUK_1:40, XXREAL_1:1;
then ((1 - t) * (f . s)) + (t * s) <= s by A15, XREAL_1:172;
then A18: ( 0 <= f . s & ((1 - t) * (f . s)) + (t * s) <= 1 ) by A16, BORSUK_1:40, XXREAL_0:2, XXREAL_1:1;
0 <= t by BORSUK_1:40, XXREAL_1:1;
then A19: f . s <= ((1 - t) * (f . s)) + (t * s) by A15, A17, XREAL_1:173;
(g1 . p) + (g2 . p) = ((1 - t) * (f . s)) + (g2 . p) by A11, A14
.= ((1 - t) * (f . s)) + (t * s) by A12, A14 ;
hence (g1 . p) + (g2 . p) is Point of I[01] by A19, A18, BORSUK_1:40, XXREAL_1:1; :: thesis:

end;

suppose A20: f . s > s ; :: thesis:

set j = 1 - t;
A21: f . s <= 1 by BORSUK_1:40, XXREAL_1:1;
A22: 1 - t in the carrier of I[01] by JORDAN5B:4;
then A23: 1 - t <= 1 by BORSUK_1:43;
then ((1 - (1 - t)) * s) + ((1 - t) * (f . s)) <= f . s by A20, XREAL_1:172;
then A24: ( 0 <= s & ((1 - t) * (f . s)) + (t * s) <= 1 ) by A21, BORSUK_1:40, XXREAL_0:2, XXREAL_1:1;
0 <= 1 - t by A22, BORSUK_1:43;
then A25: s <= ((1 - (1 - t)) * s) + ((1 - t) * (f . s)) by A20, A23, XREAL_1:173;
(g1 . p) + (g2 . p) = ((1 - t) * (f . s)) + (g2 . p) by A11, A14
.= ((1 - t) * (f . s)) + (t * s) by A12, A14 ;
hence (g1 . p) + (g2 . p) is Point of I[01] by A25, A24, BORSUK_1:40, XXREAL_1:1; :: thesis:

end;

then consider h being Function of [:I[01],I[01]:],I[01] such that
A26: for p being Point of [:I[01],I[01]:]
for r1, r2 being Real st g1 . p = r1 & g2 . p = r2 holds
h . p = r1 + r2 and
A27: h is continuous by A9, A7, Th37;
A28: for t, s being Point of I[01] holds h . [s,t] = ((1 - t) * (f . s)) + (t * s)

proof

let t, s be Point of I[01]; :: thesis:
( g1 . [s,t] = (1 - t) * (f . s) & g2 . [s,t] = t * s ) by A11, A12;
hence h . [s,t] = ((1 - t) * (f . s)) + (t * s) by A26; :: thesis:

end;

A29: for t being Point of I[01] holds h . [1,t] = 1

proof

reconsider oo = 1 as Point of I[01] by BORSUK_1:43;
let t be Point of I[01]; :: thesis:
thus h . [1,t] = ((1 - t) * (f . oo)) + (t * 1) by A28
.= 1 by A2 ; :: thesis:

end;

set H = P * h;
A30: dom h = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1
.= [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2 ;
set Q = RePar (P,f);
A31: 1 is Point of I[01] by BORSUK_1:43;
A32: for s being Point of I[01] holds h . [s,1] = s

proof

let s be Point of I[01]; :: thesis:
thus h . [s,1] = ((1 - 1) * (f . s)) + (1 * s) by A31, A28
.= s ; :: thesis:

end;

A33: 0 is Point of I[01] by BORSUK_1:43;
A34: for s being Point of I[01] holds h . [s,0] = f . s

proof

let s be Point of I[01]; :: thesis:
thus h . [s,0] = ((1 - 0) * (f . s)) + (0 * s) by A33, A28
.= f . s ; :: thesis:

end;

A35: for s being Point of I[01] holds
( (P * h) . (s,0) = (RePar (P,f)) . s & (P * h) . (s,1) = P . s )

proof

let s be Point of I[01]; :: thesis:
s in the carrier of I[01] ;
then A36: s in dom f by FUNCT_2:def 1;
0 in the carrier of I[01] by BORSUK_1:43;
then [s,0] in dom h by A30, ZFMISC_1:87;
hence (P * h) . (s,0) = P . (h . [s,0]) by FUNCT_1:13
.= P . (f . s) by A34
.= (P * f) . s by A36, FUNCT_1:13
.= (RePar (P,f)) . s by A1, A2, A3, Def4 ;
:: thesis:
1 in the carrier of I[01] by BORSUK_1:43;
then [s,1] in dom h by A30, ZFMISC_1:87;
hence (P * h) . (s,1) = P . (h . [s,1]) by FUNCT_1:13
.= P . s by A32 ;
:: thesis:

end;

A37: for t being Point of I[01] holds h . [0,t] = 0

proof

reconsider oo = 0 as Point of I[01] by BORSUK_1:43;
let t be Point of I[01]; :: thesis:
thus h . [0,t] = ((1 - t) * (f . oo)) + (t * 0) by A28
.= 0 by A1 ; :: thesis:

end;

A38: for t being Point of I[01] holds
( (P * h) . (0,t) = a & (P * h) . (1,t) = b )

proof

let t be Point of I[01]; :: thesis:
0 in the carrier of I[01] by BORSUK_1:43;
then [0,t] in dom h by A30, ZFMISC_1:87;
hence (P * h) . (0,t) = P . (h . [0,t]) by FUNCT_1:13
.= P . 0 by A37
.= a by A3, BORSUK_2:def 2 ;
:: thesis:
1 in the carrier of I[01] by BORSUK_1:43;
then [1,t] in dom h by A30, ZFMISC_1:87;
hence (P * h) . (1,t) = P . (h . [1,t]) by FUNCT_1:13
.= P . 1 by A29
.= b by A3, BORSUK_2:def 2 ;
:: thesis:

end;

P is continuous by A3, BORSUK_2:def 2;
hence RePar (P,f),P are_homotopic by A27, A35, A38; :: thesis: