let T be non empty TopSpace; :: thesis: for a, b being Point of T
for P being Path of a,b
for Q being constant Path of a,a st a,b are_connected holds
RePar (P,2RP) = Q + P
let a, b be Point of T; :: thesis: for P being Path of a,b
for Q being constant Path of a,a st a,b are_connected holds
RePar (P,2RP) = Q + P
let P be Path of a,b; :: thesis: for Q being constant Path of a,a st a,b are_connected holds
RePar (P,2RP) = Q + P
let Q be constant Path of a,a; :: thesis: ( a,b are_connected implies RePar (P,2RP) = Q + P )
assume A1: a,b are_connected ; :: thesis: RePar (P,2RP) = Q + P
set f = RePar (P,2RP);
set g = Q + P;
A2: a,a are_connected ;
for p being Element of I[01] holds (RePar (P,2RP)) . p = (Q + P) . p

proof

0 in the carrier of I[01] by BORSUK_1:43;
then A3: 0 in dom Q by FUNCT_2:def 1;
let p be Element of I[01]; :: thesis: (RePar (P,2RP)) . p = (Q + P) . p
p in the carrier of I[01] ;
then A4: p in dom 2RP by FUNCT_2:def 1;
A5: (RePar (P,2RP)) . p = (P * 2RP) . p by A1, Def4, Th48
.= P . (2RP . p) by A4, FUNCT_1:13 ;

per cases ( p <= 1 / 2 or p > 1 / 2 ) ;

suppose A6: p <= 1 / 2 ; :: thesis: (RePar (P,2RP)) . p = (Q + P) . p

then 2 * p is Point of I[01] by Th3;
then 2 * p in the carrier of I[01] ;
then A7: 2 * p in dom Q by FUNCT_2:def 1;
(RePar (P,2RP)) . p = P . 0 by A5, A6, Def6
.= a by A1, BORSUK_2:def 2
.= Q . 0 by A2, BORSUK_2:def 2
.= Q . (2 * p) by A3, A7, FUNCT_1:def 10
.= (Q + P) . p by A1, A6, BORSUK_2:def 5 ;
hence (RePar (P,2RP)) . p = (Q + P) . p ; :: thesis: verum

end;

suppose A8: p > 1 / 2 ; :: thesis: (RePar (P,2RP)) . p = (Q + P) . p

then (RePar (P,2RP)) . p = P . ((2 * p) - 1) by A5, Def6
.= (Q + P) . p by A1, A8, BORSUK_2:def 5 ;
hence (RePar (P,2RP)) . p = (Q + P) . p ; :: thesis: verum

end;

end;

end;

hence RePar (P,2RP) = Q + P by FUNCT_2:63; :: thesis: verum