let S, T be non empty TopSpace; :: thesis: for s being Point of S

for f being continuous Function of S,T st f is being_homeomorphism holds

FundGrIso (f,s) is bijective

let s be Point of S; :: thesis: for f being continuous Function of S,T st f is being_homeomorphism holds

FundGrIso (f,s) is bijective

set pS = pi_1 (S,s);

let f be continuous Function of S,T; :: thesis: ( f is being_homeomorphism implies FundGrIso (f,s) is bijective )

assume A1: f is being_homeomorphism ; :: thesis: FundGrIso (f,s) is bijective

A2: f is one-to-one by A1;

then A3: (f ") . (f . s) = s by FUNCT_2:26;

set h = FundGrIso (f,s);

set pT = pi_1 (T,(f . s));

A4: f " is continuous by A1;

A5: rng f = [#] T by A1;

then f is onto ;

then A6: f " = f " by A2, TOPS_2:def 4;

A7: dom (FundGrIso (f,s)) = the carrier of (pi_1 (S,s)) by FUNCT_2:def 1;

A8: rng (FundGrIso (f,s)) = the carrier of (pi_1 (T,(f . s)))

for f being continuous Function of S,T st f is being_homeomorphism holds

FundGrIso (f,s) is bijective

let s be Point of S; :: thesis: for f being continuous Function of S,T st f is being_homeomorphism holds

FundGrIso (f,s) is bijective

set pS = pi_1 (S,s);

let f be continuous Function of S,T; :: thesis: ( f is being_homeomorphism implies FundGrIso (f,s) is bijective )

assume A1: f is being_homeomorphism ; :: thesis: FundGrIso (f,s) is bijective

A2: f is one-to-one by A1;

then A3: (f ") . (f . s) = s by FUNCT_2:26;

set h = FundGrIso (f,s);

set pT = pi_1 (T,(f . s));

A4: f " is continuous by A1;

A5: rng f = [#] T by A1;

then f is onto ;

then A6: f " = f " by A2, TOPS_2:def 4;

A7: dom (FundGrIso (f,s)) = the carrier of (pi_1 (S,s)) by FUNCT_2:def 1;

A8: rng (FundGrIso (f,s)) = the carrier of (pi_1 (T,(f . s)))

proof

FundGrIso (f,s) is one-to-one
thus
rng (FundGrIso (f,s)) c= the carrier of (pi_1 (T,(f . s)))
; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (pi_1 (T,(f . s))) c= rng (FundGrIso (f,s))

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (pi_1 (T,(f . s))) or y in rng (FundGrIso (f,s)) )

assume y in the carrier of (pi_1 (T,(f . s))) ; :: thesis: y in rng (FundGrIso (f,s))

then consider lt being Loop of f . s such that

A9: y = Class ((EqRel (T,(f . s))),lt) by TOPALG_1:47;

reconsider ls = (f ") * lt as Loop of s by A4, A3, A6, Th26;

set x = Class ((EqRel (S,s)),ls);

A10: Class ((EqRel (S,s)),ls) in the carrier of (pi_1 (S,s)) by TOPALG_1:47;

then consider ls1 being Loop of s such that

A11: Class ((EqRel (S,s)),ls) = Class ((EqRel (S,s)),ls1) and

A12: (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls1)) by Def1;

A13: f * ls = (f * (f ")) * lt by RELAT_1:36

.= (id (rng f)) * lt by A5, A2, TOPS_2:52

.= lt by A5, FUNCT_2:17 ;

ls,ls1 are_homotopic by A11, TOPALG_1:46;

then lt,f * ls1 are_homotopic by A13, Th27;

then (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = y by A9, A12, TOPALG_1:46;

hence y in rng (FundGrIso (f,s)) by A7, A10, FUNCT_1:def 3; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (pi_1 (T,(f . s))) or y in rng (FundGrIso (f,s)) )

assume y in the carrier of (pi_1 (T,(f . s))) ; :: thesis: y in rng (FundGrIso (f,s))

then consider lt being Loop of f . s such that

A9: y = Class ((EqRel (T,(f . s))),lt) by TOPALG_1:47;

reconsider ls = (f ") * lt as Loop of s by A4, A3, A6, Th26;

set x = Class ((EqRel (S,s)),ls);

A10: Class ((EqRel (S,s)),ls) in the carrier of (pi_1 (S,s)) by TOPALG_1:47;

then consider ls1 being Loop of s such that

A11: Class ((EqRel (S,s)),ls) = Class ((EqRel (S,s)),ls1) and

A12: (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls1)) by Def1;

A13: f * ls = (f * (f ")) * lt by RELAT_1:36

.= (id (rng f)) * lt by A5, A2, TOPS_2:52

.= lt by A5, FUNCT_2:17 ;

ls,ls1 are_homotopic by A11, TOPALG_1:46;

then lt,f * ls1 are_homotopic by A13, Th27;

then (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = y by A9, A12, TOPALG_1:46;

hence y in rng (FundGrIso (f,s)) by A7, A10, FUNCT_1:def 3; :: thesis: verum

proof

hence
FundGrIso (f,s) is bijective
by A8, GROUP_6:60; :: thesis: verum
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (FundGrIso (f,s)) or not x2 in dom (FundGrIso (f,s)) or not (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 or x1 = x2 )

assume x1 in dom (FundGrIso (f,s)) ; :: thesis: ( not x2 in dom (FundGrIso (f,s)) or not (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 or x1 = x2 )

then consider ls1 being Loop of s such that

A14: x1 = Class ((EqRel (S,s)),ls1) and

A15: (FundGrIso (f,s)) . x1 = Class ((EqRel (T,(f . s))),(f * ls1)) by Def1;

assume x2 in dom (FundGrIso (f,s)) ; :: thesis: ( not (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 or x1 = x2 )

then consider ls2 being Loop of s such that

A16: x2 = Class ((EqRel (S,s)),ls2) and

A17: (FundGrIso (f,s)) . x2 = Class ((EqRel (T,(f . s))),(f * ls2)) by Def1;

reconsider a1 = (f ") * (f * ls1), a2 = (f ") * (f * ls2) as Loop of s by A4, A3, A6, Th26;

assume (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 ; :: thesis: x1 = x2

then f * ls1,f * ls2 are_homotopic by A15, A17, TOPALG_1:46;

then A18: a1,a2 are_homotopic by A4, A3, A6, Th27;

A19: (f ") * f = id (dom f) by A5, A2, TOPS_2:52;

A20: (f ") * (f * ls1) = ((f ") * f) * ls1 by RELAT_1:36

.= ls1 by A19, FUNCT_2:17 ;

(f ") * (f * ls2) = ((f ") * f) * ls2 by RELAT_1:36

.= ls2 by A19, FUNCT_2:17 ;

hence x1 = x2 by A14, A16, A20, A18, TOPALG_1:46; :: thesis: verum

end;assume x1 in dom (FundGrIso (f,s)) ; :: thesis: ( not x2 in dom (FundGrIso (f,s)) or not (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 or x1 = x2 )

then consider ls1 being Loop of s such that

A14: x1 = Class ((EqRel (S,s)),ls1) and

A15: (FundGrIso (f,s)) . x1 = Class ((EqRel (T,(f . s))),(f * ls1)) by Def1;

assume x2 in dom (FundGrIso (f,s)) ; :: thesis: ( not (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 or x1 = x2 )

then consider ls2 being Loop of s such that

A16: x2 = Class ((EqRel (S,s)),ls2) and

A17: (FundGrIso (f,s)) . x2 = Class ((EqRel (T,(f . s))),(f * ls2)) by Def1;

reconsider a1 = (f ") * (f * ls1), a2 = (f ") * (f * ls2) as Loop of s by A4, A3, A6, Th26;

assume (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 ; :: thesis: x1 = x2

then f * ls1,f * ls2 are_homotopic by A15, A17, TOPALG_1:46;

then A18: a1,a2 are_homotopic by A4, A3, A6, Th27;

A19: (f ") * f = id (dom f) by A5, A2, TOPS_2:52;

A20: (f ") * (f * ls1) = ((f ") * f) * ls1 by RELAT_1:36

.= ls1 by A19, FUNCT_2:17 ;

(f ") * (f * ls2) = ((f ") * f) * ls2 by RELAT_1:36

.= ls2 by A19, FUNCT_2:17 ;

hence x1 = x2 by A14, A16, A20, A18, TOPALG_1:46; :: thesis: verum