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

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

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

dom (P + P) = the carrier of I[01]
by FUNCT_2:def 1;
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 ;

end;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 )
;

end;

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;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

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;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

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