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

proof

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;

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