let T be non empty TopSpace; :: thesis: for a being Point of T

for P being constant Path of a,a holds - P = P

let a be Point of T; :: thesis: for P being constant Path of a,a holds - P = P

let P be constant Path of a,a; :: thesis: - P = P

A1: dom P = the carrier of I[01] by FUNCT_2:def 1;

A2: for x being object st x in the carrier of I[01] holds

P . x = (- P) . x

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

for P being constant Path of a,a holds - P = P

let a be Point of T; :: thesis: for P being constant Path of a,a holds - P = P

let P be constant Path of a,a; :: thesis: - P = P

A1: dom P = the carrier of I[01] by FUNCT_2:def 1;

A2: for x being object st x in the carrier of I[01] holds

P . x = (- P) . x

proof

dom (- 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) . x )

assume A3: x in the carrier of I[01] ; :: thesis: P . x = (- P) . x

then reconsider x2 = x as Real ;

reconsider x3 = 1 - x2 as Point of I[01] by A3, Lm5;

(- P) . x = P . x3 by A3, Def6

.= P . x by A1, A3, FUNCT_1:def 10 ;

hence P . x = (- P) . x ; :: thesis: verum

end;assume A3: x in the carrier of I[01] ; :: thesis: P . x = (- P) . x

then reconsider x2 = x as Real ;

reconsider x3 = 1 - x2 as Point of I[01] by A3, Lm5;

(- P) . x = P . x3 by A3, Def6

.= P . x by A1, A3, FUNCT_1:def 10 ;

hence P . x = (- P) . x ; :: thesis: verum

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