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