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 Th31;
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:50;
G is bijective by A2, TOPALG_1:55;
hence h is bijective by A1, A3, GROUP_6:64; :: thesis: verum