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