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 set ; :: 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 Th48;
A3: (P + (((- P) + Y) + P)) + (- P),Y are_homotopic by A1, Th42;
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 Th48;
(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, Th47 ;
hence y in rng (pi_1-iso P) by A4, FUNCT_1:def 5; :: thesis: verum