let T be non empty TopSpace; :: thesis:
let a, b be Point of T; :: thesis:
let P be Path of a,b; :: thesis:
let f be continuous Function of I[01] ,I[01] ; :: thesis:
assume A1: ( f . 0 = 0 & f . 1 = 1 & a,b are_connected ) ; :: thesis:
set Q = RePar P,f;
A2: ( 0 is Point of I[01] & 1 is Point of I[01] ) by BORSUK_1:86;
set X = [:I[01] ,I[01] :];
reconsider ID = id I[01] as Path of 0[01] , 1[01] by Th12;
set G1 = - ID;
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 f1 = (- ID) * G2 as continuous Function of [:I[01] ,I[01] :],I[01] ;
A3: for s, t being Point of I[01] holds f1 . [s,t] = 1 - t

proof

let s, t be Point of I[01] ; :: thesis:
A4: 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:106;
then [s,t] in dom G2 by FUNCT_2:def 1;
then f1 . [s,t] = (- ID) . (G2 . s,t) by FUNCT_1:23
.= (- ID) . t by FUNCT_3:def 6
.= ID . (1 - t) by Def5
.= 1 - t by A4, TMAP_1:91 ;
hence f1 . [s,t] = 1 - t ; :: thesis:

end;

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 f2 = f * F2 as continuous Function of [:I[01] ,I[01] :],I[01] ;
A5: 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:106;
then [s,t] in dom F2 by FUNCT_2:def 1;
hence f2 . s,t = f . (F2 . s,t) by FUNCT_1:23
.= f . s by FUNCT_3:def 5 ;
:: thesis:

end;

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;
A6: for p being Point of [:I[01] ,I[01] :] holds (f1 . p) * (f2 . p) is Point of I[01] by Th8;
A7: for p being Point of [:I[01] ,I[01] :] holds (f3 . p) * (f4 . p) is Point of I[01] by Th8;
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 number st f1 . p = r1 & f2 . p = r2 holds
g1 . p = r1 * r2 ) & g1 is continuous ) by A6, Th40;
A9: 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 A3, A5;
hence g1 . [s,t] = (1 - t) * (f . s) by A8; :: thesis:

end;

consider g2 being Function of [:I[01] ,I[01] :],I[01] such that
A10: ( ( for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st f3 . p = r1 & f4 . p = r2 holds
g2 . p = r1 * r2 ) & g2 is continuous ) by A7, Th40;
A11: 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 5, FUNCT_3:def 6;
hence g2 . [s,t] = t * s by A10; :: 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 5;
then consider s, t being set such that
A12: ( s in the carrier of I[01] & t in the carrier of I[01] & p = [s,t] ) by ZFMISC_1:def 2;
reconsider s = s, t = t as Point of I[01] by A12;
set a = f . s;

per cases ;

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

( 0 <= t & t <= 1 ) by BORSUK_1:83, XXREAL_1:1;
then A14: ( f . s <= ((1 - t) * (f . s)) + (t * s) & ((1 - t) * (f . s)) + (t * s) <= s ) by A13, XREAL_1:174, XREAL_1:175;
A15: (g1 . p) + (g2 . p) = ((1 - t) * (f . s)) + (g2 . p) by A9, A12
.= ((1 - t) * (f . s)) + (t * s) by A11, A12 ;
A16: 0 <= f . s by BORSUK_1:83, XXREAL_1:1;
s <= 1 by BORSUK_1:83, XXREAL_1:1;
then ((1 - t) * (f . s)) + (t * s) <= 1 by A14, XXREAL_0:2;
hence (g1 . p) + (g2 . p) is Point of I[01] by A14, A15, A16, BORSUK_1:83, XXREAL_1:1; :: thesis:

end;

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

set j = 1 - t;
1 - t in the carrier of I[01] by JORDAN5B:4;
then ( 0 <= 1 - t & 1 - t <= 1 ) by BORSUK_1:86;
then A18: ( s <= ((1 - (1 - t)) * s) + ((1 - t) * (f . s)) & ((1 - (1 - t)) * s) + ((1 - t) * (f . s)) <= f . s ) by A17, XREAL_1:174, XREAL_1:175;
A19: (g1 . p) + (g2 . p) = ((1 - t) * (f . s)) + (g2 . p) by A9, A12
.= ((1 - t) * (f . s)) + (t * s) by A11, A12 ;
A20: 0 <= s by BORSUK_1:83, XXREAL_1:1;
f . s <= 1 by BORSUK_1:83, XXREAL_1:1;
then ((1 - t) * (f . s)) + (t * s) <= 1 by A18, XXREAL_0:2;
hence (g1 . p) + (g2 . p) is Point of I[01] by A18, A19, A20, BORSUK_1:83, XXREAL_1:1; :: thesis:

end;

then consider h being Function of [:I[01] ,I[01] :],I[01] such that
A21: ( ( for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st g1 . p = r1 & g2 . p = r2 holds
h . p = r1 + r2 ) & h is continuous ) by A8, A10, Th41;
A22: 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 A9, A11;
hence h . [s,t] = ((1 - t) * (f . s)) + (t * s) by A21; :: thesis:

end;

A23: 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 A2, A22
.= f . s ; :: thesis:

end;

A24: 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 A2, A22
.= s ; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

A27: 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 5 ;
set H = P * h;
P is continuous by A1, BORSUK_2:def 2;
then A28: P * h is continuous by A21;
A29: 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] & 0 in the carrier of I[01] ) by BORSUK_1:86;
then A30: [s,0 ] in dom h by A27, ZFMISC_1:106;
1 in the carrier of I[01] by BORSUK_1:86;
then A31: [s,1] in dom h by A27, ZFMISC_1:106;
s in the carrier of I[01] ;
then A32: s in dom f by FUNCT_2:def 1;
thus (P * h) . s,0 = P . (h . [s,0 ]) by A30, FUNCT_1:23
.= P . (f . s) by A23
.= (P * f) . s by A32, FUNCT_1:23
.= (RePar P,f) . s by A1, Def6 ; :: thesis:
thus (P * h) . s,1 = P . (h . [s,1]) by A31, FUNCT_1:23
.= P . s by A24 ; :: thesis:

end;

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:
( t in the carrier of I[01] & 0 in the carrier of I[01] ) by BORSUK_1:86;
then A33: [0 ,t] in dom h by A27, ZFMISC_1:106;
1 in the carrier of I[01] by BORSUK_1:86;
then A34: [1,t] in dom h by A27, ZFMISC_1:106;
thus (P * h) . 0 ,t = P . (h . [0 ,t]) by A33, FUNCT_1:23
.= P . 0 by A25
.= a by A1, BORSUK_2:def 2 ; :: thesis:
thus (P * h) . 1,t = P . (h . [1,t]) by A34, FUNCT_1:23
.= P . 1 by A26
.= b by A1, BORSUK_2:def 2 ; :: thesis:

end;

hence RePar P,f,P are_homotopic by A28, A29, BORSUK_2:def 7; :: thesis: