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: dom (P + P) = the carrier of I[01] by FUNCT_2:def 1;
A2: the carrier of I[01] = dom P by FUNCT_2:def 1;
for x being set st x in the carrier of I[01] holds
P . x = (P + P) . x

proof

let x be set ; :: 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:83, RCOMP_1:def 1;
then consider r being Real such that
A4: ( r = x & 0 <= r & r <= 1 ) ;

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

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

A6: 2 * r >= 0 by A4, XREAL_1:129;
r * 2 < (1 / 2) * 2 by A5, XREAL_1:70;
then 2 * r in { e where e is Real : ( 0 <= e & e <= 1 ) } by A6;
then 2 * r in the carrier of I[01] by BORSUK_1:83, RCOMP_1:def 1;
then P . (2 * r) = P . p by A2, FUNCT_1:def 16;
hence P . x = (P + P) . x by A4, A5, Def5; :: thesis: verum

end;

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

then r * 2 >= (1 / 2) * 2 by XREAL_1:66;
then 2 * r >= 1 + 0 ;
then A8: (2 * r) - 1 >= 0 by XREAL_1:21;
r * 2 <= 1 * 2 by A4, XREAL_1:66;
then (2 * r) - 1 <= 2 - 1 by XREAL_1:15;
then (2 * r) - 1 in { e where e is Real : ( 0 <= e & e <= 1 ) } by A8;
then (2 * r) - 1 in the carrier of I[01] by BORSUK_1:83, RCOMP_1:def 1;
then P . ((2 * r) - 1) = P . p by A2, FUNCT_1:def 16;
hence P . x = (P + P) . x by A4, A7, Def5; :: thesis: verum

end;

end;

end;

hence P + P = P by A1, A2, FUNCT_1:9; :: thesis: verum