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 b,b st a,b are_connected holds
RePar P,1RP = P + Q
let a, b be Point of T; :: thesis: for P being Path of a,b
for Q being constant Path of b,b st a,b are_connected holds
RePar P,1RP = P + Q
let P be Path of a,b; :: thesis: for Q being constant Path of b,b st a,b are_connected holds
RePar P,1RP = P + Q
let Q be constant Path of b,b; :: thesis: ( a,b are_connected implies RePar P,1RP = P + Q )
set f = RePar P,1RP ;
set g = P + Q;
assume A1: a,b are_connected ; :: thesis: RePar P,1RP = P + Q
A2: b,b are_connected ;
for p being Element of I[01] holds (RePar P,1RP ) . p = (P + Q) . p

proof

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

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

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

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

end;

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

then (2 * p) - 1 is Point of I[01] by Th7;
then (2 * p) - 1 in the carrier of I[01] ;
then A8: (2 * p) - 1 in dom Q by FUNCT_2:def 1;
(RePar P,1RP ) . p = P . 1 by A5, A7, Def7
.= b by A1, BORSUK_2:def 2
.= Q . 0 by A2, BORSUK_2:def 2
.= Q . ((2 * p) - 1) by A3, A8, FUNCT_1:def 16
.= (P + Q) . p by A1, A7, BORSUK_2:def 5 ;
hence (RePar P,1RP ) . p = (P + Q) . p ; :: thesis: verum

end;

end;

end;

hence RePar P,1RP = P + Q by FUNCT_2:113; :: thesis: verum