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 is onto
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 is onto
let P be Path of x0,x1; :: thesis: ( x0,x1 are_connected implies pi_1-iso P is onto )
assume A1: x0,x1 are_connected ; :: thesis: pi_1-iso P is onto
set f = pi_1-iso P;
thus rng (pi_1-iso P) c= the carrier of (pi_1 (X,x0)) ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of (pi_1 (X,x0)) c= rng (pi_1-iso P)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (pi_1 (X,x0)) or y in rng (pi_1-iso P) )
assume y in the carrier of (pi_1 (X,x0)) ; :: thesis: y in rng (pi_1-iso P)
then consider Y being Loop of x0 such that
A2: y = Class ((EqRel (X,x0)),Y) by Th47;
A3: (P + (((- P) + Y) + P)) + (- P),Y are_homotopic by A1, Th41;
set Z = Class ((EqRel (X,x1)),(((- P) + Y) + P));
dom (pi_1-iso P) = the carrier of (pi_1 (X,x1)) by FUNCT_2:def 1;
then A4: Class ((EqRel (X,x1)),(((- P) + Y) + P)) in dom (pi_1-iso P) by Th47;
(pi_1-iso P) . (Class ((EqRel (X,x1)),(((- P) + Y) + P))) = Class ((EqRel (X,x0)),((P + (((- P) + Y) + P)) + (- P))) by A1, Def6
.= y by A2, A3, Th46 ;
hence y in rng (pi_1-iso P) by A4, FUNCT_1:def 3; :: thesis: verum