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 = () * (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 = () * (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 = () * (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 = () * (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 = () * (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 = () * (FundGrIso (f,s)) implies h is bijective )
assume f is being_homeomorphism ; :: thesis: ( not f . s,t are_connected or not h = () * (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 = () * (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 ;
G is bijective by ;
hence h is bijective by ; :: thesis: verum