let T be non empty TopSpace; :: thesis: for a being Point of T
for P being constant Path of a,a holds P + P = P
let a be Point of T; :: thesis: for P being constant Path of a,a holds P + P = P
let P be constant Path of a,a; :: thesis: P + P = P
A1: the carrier of I[01] = dom P by FUNCT_2:def 1;
A2: for x being object st x in the carrier of I[01] holds
P . x = (P + P) . x

proof

let x be object ; :: thesis: ( x in the carrier of I[01] implies P . x = (P + P) . x )
assume A3: x in the carrier of I[01] ; :: thesis: P . x = (P + P) . x
then reconsider p = x as Point of I[01] ;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A3, BORSUK_1:40, RCOMP_1:def 1;
then consider r being Real such that
A4: r = x and
A5: 0 <= r and
A6: r <= 1 ;

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

suppose A7: r < 1 / 2 ; :: thesis: P . x = (P + P) . x

then A8: r * 2 < (1 / 2) * 2 by XREAL_1:68;
2 * r >= 0 by A5, XREAL_1:127;
then 2 * r in { e where e is Real : ( 0 <= e & e <= 1 ) } by A8;
then 2 * r in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def 1;
then P . (2 * r) = P . p by A1, FUNCT_1:def 10;
hence P . x = (P + P) . x by A4, A7, Def5; :: thesis: verum

end;

suppose A9: r >= 1 / 2 ; :: thesis: P . x = (P + P) . x

then r * 2 >= (1 / 2) * 2 by XREAL_1:64;
then 2 * r >= 1 + 0 ;
then A10: (2 * r) - 1 >= 0 by XREAL_1:19;
r * 2 <= 1 * 2 by A6, XREAL_1:64;
then (2 * r) - 1 <= 2 - 1 by XREAL_1:13;
then (2 * r) - 1 in { e where e is Real : ( 0 <= e & e <= 1 ) } by A10;
then (2 * r) - 1 in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def 1;
then P . ((2 * r) - 1) = P . p by A1, FUNCT_1:def 10;
hence P . x = (P + P) . x by A4, A9, Def5; :: thesis: verum

end;

end;

end;

dom (P + P) = the carrier of I[01] by FUNCT_2:def 1;
hence P + P = P by A1, A2, FUNCT_1:2; :: thesis: verum