let S, T be non empty TopSpace; :: thesis: for s1, s2 being Point of S
for t1, t2 being Point of T st s1,s2 are_connected & t1,t2 are_connected holds
[s1,t1],[s2,t2] are_connected
let s1, s2 be Point of S; :: thesis: for t1, t2 being Point of T st s1,s2 are_connected & t1,t2 are_connected holds
[s1,t1],[s2,t2] are_connected
let t1, t2 be Point of T; :: thesis: ( s1,s2 are_connected & t1,t2 are_connected implies [s1,t1],[s2,t2] are_connected )
given f being Function of I[01],S such that A1: f is continuous and
A2: f . 0 = s1 and
A3: f . 1 = s2 ; :: according to BORSUK_2:def 1 :: thesis: ( not t1,t2 are_connected or [s1,t1],[s2,t2] are_connected )
given g being Function of I[01],T such that A4: g is continuous and
A5: g . 0 = t1 and
A6: g . 1 = t2 ; :: according to BORSUK_2:def 1 :: thesis: [s1,t1],[s2,t2] are_connected
take <:f,g:> ; :: according to BORSUK_2:def 1 :: thesis: ( <:f,g:> is continuous & <:f,g:> . 0 = [s1,t1] & <:f,g:> . 1 = [s2,t2] )
thus <:f,g:> is continuous by A1, A4, YELLOW12:41; :: thesis: ( <:f,g:> . 0 = [s1,t1] & <:f,g:> . 1 = [s2,t2] )
A7: ( dom f = the carrier of I[01] & dom g = the carrier of I[01] ) by FUNCT_2:def 1;
hence <:f,g:> . 0 = [(f . j0),(g . j0)] by FUNCT_3:49
.= [s1,t1] by A2, A5 ;
:: thesis: <:f,g:> . 1 = [s2,t2]
thus <:f,g:> . 1 = [(f . j1),(g . j1)] by A7, FUNCT_3:49
.= [s2,t2] by A3, A6 ; :: thesis: verum