let T be non empty pathwise_connected TopSpace; :: thesis: for y0, y1 being Point of T
for R, V being Path of y0,y1 st R,V are_homotopic holds
pi_1-iso R = pi_1-iso V
let y0, y1 be Point of T; :: thesis: for R, V being Path of y0,y1 st R,V are_homotopic holds
pi_1-iso R = pi_1-iso V
let R, V be Path of y0,y1; :: thesis: ( R,V are_homotopic implies pi_1-iso R = pi_1-iso V )
y0,y1 are_connected by BORSUK_2:def 3;
hence ( R,V are_homotopic implies pi_1-iso R = pi_1-iso V ) by Th49; :: thesis: verum