let X be non empty TopSpace; :: thesis: for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
(pi_1-iso P) " = pi_1-iso (- P)
let x0, x1 be Point of X; :: thesis: for P being Path of x0,x1 st x0,x1 are_connected holds
(pi_1-iso P) " = pi_1-iso (- P)
let P be Path of x0,x1; :: thesis: ( x0,x1 are_connected implies (pi_1-iso P) " = pi_1-iso (- P) )
set f = pi_1-iso P;
set g = pi_1-iso (- P);
assume A1: x0,x1 are_connected ; :: thesis: (pi_1-iso P) " = pi_1-iso (- P)
then ( pi_1-iso P is one-to-one & pi_1-iso P is onto ) by Th51, Th52;
then A2: (pi_1-iso P) " = (pi_1-iso P) " by TOPS_2:def 4;
A3: pi_1-iso P is one-to-one by A1, Th51;
for x being Element of (pi_1 (X,x0)) holds ((pi_1-iso P) ") . x = (pi_1-iso (- P)) . x

proof

let x be Element of (pi_1 (X,x0)); :: thesis: ((pi_1-iso P) ") . x = (pi_1-iso (- P)) . x
consider Q being Loop of x0 such that
A4: x = Class ((EqRel (X,x0)),Q) by Th47;
- (- P) = P by A1, BORSUK_6:43;
then A5: (P + (((- P) + Q) + (- (- P)))) + (- P),Q are_homotopic by A1, Th41;
dom (pi_1-iso P) = the carrier of (pi_1 (X,x1)) by FUNCT_2:def 1;
then A6: Class ((EqRel (X,x1)),(((- P) + Q) + (- (- P)))) in dom (pi_1-iso P) by Th47;
(pi_1-iso P) . (Class ((EqRel (X,x1)),(((- P) + Q) + (- (- P))))) = Class ((EqRel (X,x0)),((P + (((- P) + Q) + (- (- P)))) + (- P))) by A1, Def6
.= x by A4, A5, Th46 ;
hence ((pi_1-iso P) ") . x = Class ((EqRel (X,x1)),(((- P) + Q) + (- (- P)))) by A3, A2, A6, FUNCT_1:32
.= (pi_1-iso (- P)) . x by A1, A4, Def6 ;
:: thesis: verum

end;

hence (pi_1-iso P) " = pi_1-iso (- P) ; :: thesis: verum