let S, T be non empty TopSpace; :: thesis: for f being continuous Function of S,T

for a, b being Point of S st a,b are_connected holds

f . a,f . b are_connected

let f be continuous Function of S,T; :: thesis: for a, b being Point of S st a,b are_connected holds

f . a,f . b are_connected

let a, b be Point of S; :: thesis: ( a,b are_connected implies f . a,f . b are_connected )

given g being Function of I[01],S such that A1: g is continuous and

A2: g . 0 = a and

A3: g . 1 = b ; :: according to BORSUK_2:def 1 :: thesis: f . a,f . b are_connected

take h = f * g; :: according to BORSUK_2:def 1 :: thesis: ( h is continuous & h . 0 = f . a & h . 1 = f . b )

thus h is continuous by A1; :: thesis: ( h . 0 = f . a & h . 1 = f . b )

thus h . 0 = f . (g . j0) by FUNCT_2:15

.= f . a by A2 ; :: thesis: h . 1 = f . b

thus h . 1 = f . (g . j1) by FUNCT_2:15

.= f . b by A3 ; :: thesis: verum

for a, b being Point of S st a,b are_connected holds

f . a,f . b are_connected

let f be continuous Function of S,T; :: thesis: for a, b being Point of S st a,b are_connected holds

f . a,f . b are_connected

let a, b be Point of S; :: thesis: ( a,b are_connected implies f . a,f . b are_connected )

given g being Function of I[01],S such that A1: g is continuous and

A2: g . 0 = a and

A3: g . 1 = b ; :: according to BORSUK_2:def 1 :: thesis: f . a,f . b are_connected

take h = f * g; :: according to BORSUK_2:def 1 :: thesis: ( h is continuous & h . 0 = f . a & h . 1 = f . b )

thus h is continuous by A1; :: thesis: ( h . 0 = f . a & h . 1 = f . b )

thus h . 0 = f . (g . j0) by FUNCT_2:15

.= f . a by A2 ; :: thesis: h . 1 = f . b

thus h . 1 = f . (g . j1) by FUNCT_2:15

.= f . b by A3 ; :: thesis: verum