let S, T be non empty TopSpace; :: thesis: for f being Function of S,T
for A being Subset of T st f is being_homeomorphism & A is connected holds
f " A is connected
let f be Function of S,T; :: thesis: for A being Subset of T st f is being_homeomorphism & A is connected holds
f " A is connected
let A be Subset of T; :: thesis: ( f is being_homeomorphism & A is connected implies f " A is connected )
assume that
A1: f is being_homeomorphism and
A2: A is connected ; :: thesis: f " A is connected
f " is continuous by A1;
then A3: (f ") .: A is connected by A2, Th61;
( rng f = [#] T & f is one-to-one ) by A1;
hence f " A is connected by A3, Th55; :: thesis: verum