let S, T be non empty TopSpace; :: thesis: for s being Point of S
for t being Point of T
for f being continuous Function of S,T
for P being Path of t,f . s
for h being Homomorphism of (pi_1 S,s),(pi_1 T,t) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso f,s) holds
h is bijective
let s be Point of S; :: thesis: for t being Point of T
for f being continuous Function of S,T
for P being Path of t,f . s
for h being Homomorphism of (pi_1 S,s),(pi_1 T,t) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso f,s) holds
h is bijective
let t be Point of T; :: thesis: for f being continuous Function of S,T
for P being Path of t,f . s
for h being Homomorphism of (pi_1 S,s),(pi_1 T,t) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso f,s) holds
h is bijective
let f be continuous Function of S,T; :: thesis: for P being Path of t,f . s
for h being Homomorphism of (pi_1 S,s),(pi_1 T,t) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso f,s) holds
h is bijective
let P be Path of t,f . s; :: thesis: for h being Homomorphism of (pi_1 S,s),(pi_1 T,t) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso f,s) holds
h is bijective
let h be Homomorphism of (pi_1 S,s),(pi_1 T,t); :: thesis: ( f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso f,s) implies h is bijective )
assume f is being_homeomorphism ; :: thesis: ( not f . s,t are_connected or not h = (pi_1-iso P) * (FundGrIso f,s) or h is bijective )
then A1: FundGrIso f,s is bijective by Th33;
assume that
A2: f . s,t are_connected and
A3: h = (pi_1-iso P) * (FundGrIso f,s) ; :: thesis: h is bijective
reconsider G = pi_1-iso P as Homomorphism of (pi_1 T,(f . s)),(pi_1 T,t) by A2, TOPALG_1:51;
G is bijective by A2, TOPALG_1:56;
hence h is bijective by A1, A3, GROUP_6:74; :: thesis: verum