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
for L1 being Path of s1,s2
for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2]
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
for L1 being Path of s1,s2
for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2]
let t1, t2 be Point of T; :: thesis: ( s1,s2 are_connected & t1,t2 are_connected implies for L1 being Path of s1,s2
for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2] )
assume that
A1: s1,s2 are_connected and
A2: t1,t2 are_connected ; :: thesis: for L1 being Path of s1,s2
for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2]
let L1 be Path of s1,s2; :: thesis: for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2]
let L2 be Path of t1,t2; :: thesis: <:L1,L2:> is Path of [s1,t1],[s2,t2]
( L1 is continuous & L2 is continuous ) by A1, A2, BORSUK_2:def 2;
then A3: <:L1,L2:> is continuous by YELLOW12:41;
A4: ( dom L1 = the carrier of I[01] & dom L2 = the carrier of I[01] ) by FUNCT_2:def 1;
then A5: <:L1,L2:> . j1 = [(L1 . j1),(L2 . j1)] by FUNCT_3:49
.= [s2,(L2 . j1)] by A1, BORSUK_2:def 2
.= [s2,t2] by A2, BORSUK_2:def 2 ;
A6: <:L1,L2:> . j0 = [(L1 . j0),(L2 . j0)] by A4, FUNCT_3:49
.= [s1,(L2 . j0)] by A1, BORSUK_2:def 2
.= [s1,t1] by A2, BORSUK_2:def 2 ;
then [s1,t1],[s2,t2] are_connected by A3, A5;
hence <:L1,L2:> is Path of [s1,t1],[s2,t2] by A3, A6, A5, BORSUK_2:def 2; :: thesis: verum