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 = dom P by FUNCT_2:def 1;
A2: for x being object st x in the carrier of I holds
P . x = (P + P) . x
proof
let x be object ; :: thesis: ( x in the carrier of I implies P . x = (P + P) . x )
assume A3: x in the carrier of I ; :: thesis: P . x = (P + P) . x
then reconsider p = x as Point of I ;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by ;
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 ;
then 2 * r in { e where e is Real : ( 0 <= e & e <= 1 ) } by A8;
then 2 * r in the carrier of I by ;
then P . (2 * r) = P . p by ;
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 ;
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 by ;
then P . ((2 * r) - 1) = P . p by ;
hence P . x = (P + P) . x by A4, A9, Def5; :: thesis: verum
end;
end;
end;
dom (P + P) = the carrier of I by FUNCT_2:def 1;
hence P + P = P by ; :: thesis: verum