let S, T be non empty TopSpace; :: thesis: ( S,T are_homeomorphic & S is having_trivial_Fundamental_Group implies T is having_trivial_Fundamental_Group )

given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: ( not S is having_trivial_Fundamental_Group or T is having_trivial_Fundamental_Group )

assume A2: for s being Point of S holds pi_1 (S,s) is trivial ; :: according to TOPALG_6:def 1 :: thesis: T is having_trivial_Fundamental_Group

let t be Point of T; :: according to TOPALG_6:def 1 :: thesis: pi_1 (T,t) is trivial

rng f = [#] T by A1, TOPS_2:def 5;

then consider s being Point of S such that

A3: f . s = t by FUNCT_2:113;

A4: FundGrIso (f,s) is bijective by A1, TOPALG_3:31;

pi_1 (S,s) is trivial by A2;

hence pi_1 (T,t) is trivial by A3, A4, KNASTER:11, TOPREALC:1; :: thesis: verum

given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: ( not S is having_trivial_Fundamental_Group or T is having_trivial_Fundamental_Group )

assume A2: for s being Point of S holds pi_1 (S,s) is trivial ; :: according to TOPALG_6:def 1 :: thesis: T is having_trivial_Fundamental_Group

let t be Point of T; :: according to TOPALG_6:def 1 :: thesis: pi_1 (T,t) is trivial

rng f = [#] T by A1, TOPS_2:def 5;

then consider s being Point of S such that

A3: f . s = t by FUNCT_2:113;

A4: FundGrIso (f,s) is bijective by A1, TOPALG_3:31;

pi_1 (S,s) is trivial by A2;

hence pi_1 (T,t) is trivial by A3, A4, KNASTER:11, TOPREALC:1; :: thesis: verum