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

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