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 onto by Th53;
then rng (pi_1-iso P) = the carrier of (pi_1 X,x0) by FUNCT_2:def 3;
then A2: (pi_1-iso P) " = (pi_1-iso P) " by A1, Th52, TOPS_2:def 4;
A3: pi_1-iso P is one-to-one by A1, Th52;
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 Th48;
- (- P) = P by A1, BORSUK_6:50;
then A5: (P + (((- P) + Q) + (- (- P)))) + (- P),Q are_homotopic by A1, Th42;
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 Th48;
(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, Th47 ;
hence ((pi_1-iso P) " ) . x = Class (EqRel X,x1),(((- P) + Q) + (- (- P))) by A3, A2, A6, FUNCT_1:54
.= (pi_1-iso (- P)) . x by A1, A4, Def6 ;
:: thesis: verum

end;

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