let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: ( 2 <= len f1 & 2 <= len f2 & f1 is special & f2 is special & ( for n being Nat st n in dom f1 & n + 1 in dom f1 holds
f1 /. n <> f1 /. (n + 1) ) & ( for n being Nat st n in dom f2 & n + 1 in dom f2 holds
f2 /. n <> f2 /. (n + 1) ) & X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) & Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) implies L~ f1 meets L~ f2 )
assume that
A1: 2 <= len f1 and
A2: 2 <= len f2 and
A3: f1 is special and
A4: f2 is special and
A5: for n being Nat st n in dom f1 & n + 1 in dom f1 holds
f1 /. n <> f1 /. (n + 1) and
A6: for n being Nat st n in dom f2 & n + 1 in dom f2 holds
f2 /. n <> f2 /. (n + 1) and
A7: X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) and
A8: X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) and
A9: Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) and
A10: Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) ; :: thesis: L~ f1 meets L~ f2
( len f1 <> 0 & len f2 <> 0 ) by A1, A2;
then reconsider f1 = f1, f2 = f2 as non empty FinSequence of (TOP-REAL 2) ;
reconsider f = f1 ^ f2 as non empty FinSequence of (TOP-REAL 2) ;
A11: Seg (len f2) = dom f2 by FINSEQ_1:def 3;
reconsider p1 = f1 /. 1, p2 = f1 /. (len f1), q1 = f2 /. 1, q2 = f2 /. (len f2) as Point of (TOP-REAL 2) ;
set x = X_axis f;
set y = Y_axis f;
set x1 = X_axis f1;
set y1 = Y_axis f1;
set x2 = X_axis f2;
set y2 = Y_axis f2;
A12: Seg (len f1) = dom f1 by FINSEQ_1:def 3;
A13: 1 <= len f1 by A1, XXREAL_0:2;
then A14: 1 in dom f1 by FINSEQ_3:25;
then A15: f /. 1 = f1 /. 1 by FINSEQ_4:68;
A16: Seg (len f) = dom f by FINSEQ_1:def 3;
set G = GoB f;
A17: ( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def 3, GOBOARD1:def 1;
A18: ( Seg (len (X_axis f2)) = dom (X_axis f2) & len (X_axis f2) = len f2 ) by FINSEQ_1:def 3, GOBOARD1:def 1;
A19: len f = (len f1) + (len f2) by FINSEQ_1:22;
A20: ( Seg (len (X_axis f1)) = dom (X_axis f1) & len (X_axis f1) = len f1 ) by FINSEQ_1:def 3, GOBOARD1:def 1;
then A21: (X_axis f1) . 1 = p1 `1 by A12, A14, GOBOARD1:def 1;

A22: now :: thesis: for m being Nat st m in dom f holds
p1 `1 <= (X_axis f) . m

let m be Nat; :: thesis: ( m in dom f implies p1 `1 <= (X_axis f) . m )
set s = (X_axis f) . m;
assume A23: m in dom f ; :: thesis: p1 `1 <= (X_axis f) . m
then A24: m <= len f by FINSEQ_3:25;
A25: 1 <= m by A23, FINSEQ_3:25;

now :: thesis: p1 `1 <= (X_axis f) . m

per cases ( m <= len f1 or len f1 < m ) ;

suppose A26: m <= len f1 ; :: thesis: p1 `1 <= (X_axis f) . m

reconsider u = f1 /. m as Point of (TOP-REAL 2) ;
A27: m in dom f1 by A25, A26, FINSEQ_3:25;
then f /. m = u by FINSEQ_4:68;
then A28: (X_axis f) . m = u `1 by A16, A17, A23, GOBOARD1:def 1;
(X_axis f1) . m = u `1 by A12, A20, A27, GOBOARD1:def 1;
hence p1 `1 <= (X_axis f) . m by A7, A12, A20, A21, A27, A28; :: thesis: verum

end;

suppose A29: len f1 < m ; :: thesis: p1 `1 <= (X_axis f) . m

then reconsider w5 = m - (len f1) as Element of NAT by INT_1:5;
w5 > 0 by A29, XREAL_1:50;
then A30: 1 <= w5 by NAT_1:14;
A31: m = w5 + (len f1) ;
then reconsider m1 = m - (len f1) as Nat ;
reconsider u = f2 /. m1 as Point of (TOP-REAL 2) ;
A32: w5 <= len f2 by A19, A24, A31, XREAL_1:6;
then f /. m = f2 /. w5 by A31, A30, SEQ_4:136;
then A33: (X_axis f) . m = u `1 by A16, A17, A23, GOBOARD1:def 1;
A34: m1 in dom f2 by A30, A32, FINSEQ_3:25;
then (X_axis f2) . m1 = u `1 by A11, A18, GOBOARD1:def 1;
hence p1 `1 <= (X_axis f) . m by A8, A11, A18, A21, A34, A33; :: thesis: verum

end;

end;

end;

hence p1 `1 <= (X_axis f) . m ; :: thesis: verum

end;

len f = (len f1) + (len f2) by FINSEQ_1:22;
then 2 + 2 <= len f by A1, A2, XREAL_1:7;
then 1 <= len f by XXREAL_0:2;
then A35: 1 in dom f by FINSEQ_3:25;
then (X_axis f) . 1 = p1 `1 by A16, A17, A15, GOBOARD1:def 1;
then A36: f /. 1 in rng (Line ((GoB f),1)) by A35, A22, GOBOARD2:15;
A37: len f1 in dom f1 by A13, FINSEQ_3:25;
then A38: f /. (len f1) = f1 /. (len f1) by FINSEQ_4:68;
A39: (X_axis f1) . (len f1) = p2 `1 by A12, A20, A37, GOBOARD1:def 1;

A40: now :: thesis: for m being Nat st m in dom f holds
(X_axis f) . m <= p2 `1

let m be Nat; :: thesis: ( m in dom f implies (X_axis f) . m <= p2 `1 )
set s = (X_axis f) . m;
assume A41: m in dom f ; :: thesis: (X_axis f) . m <= p2 `1
then A42: m <= len f by FINSEQ_3:25;
A43: 1 <= m by A41, FINSEQ_3:25;

now :: thesis: (X_axis f) . m <= p2 `1

per cases ( m <= len f1 or len f1 < m ) ;

suppose A44: m <= len f1 ; :: thesis: (X_axis f) . m <= p2 `1

reconsider u = f1 /. m as Point of (TOP-REAL 2) ;
A45: m in dom f1 by A43, A44, FINSEQ_3:25;
then f /. m = u by FINSEQ_4:68;
then A46: (X_axis f) . m = u `1 by A16, A17, A41, GOBOARD1:def 1;
(X_axis f1) . m = u `1 by A12, A20, A45, GOBOARD1:def 1;
hence (X_axis f) . m <= p2 `1 by A7, A12, A20, A39, A45, A46; :: thesis: verum

end;

suppose A47: len f1 < m ; :: thesis: (X_axis f) . m <= p2 `1

then reconsider w5 = m - (len f1) as Element of NAT by INT_1:5;
w5 > 0 by A47, XREAL_1:50;
then A48: 1 <= w5 by NAT_1:14;
A49: m = w5 + (len f1) ;
then reconsider m1 = m - (len f1) as Nat ;
reconsider u = f2 /. m1 as Point of (TOP-REAL 2) ;
A50: w5 <= len f2 by A19, A42, A49, XREAL_1:6;
then f /. m = f2 /. w5 by A49, A48, SEQ_4:136;
then A51: (X_axis f) . m = u `1 by A16, A17, A41, GOBOARD1:def 1;
A52: m1 in dom f2 by A48, A50, FINSEQ_3:25;
then (X_axis f2) . m1 = u `1 by A11, A18, GOBOARD1:def 1;
hence (X_axis f) . m <= p2 `1 by A8, A11, A18, A39, A52, A51; :: thesis: verum

end;

end;

end;

hence (X_axis f) . m <= p2 `1 ; :: thesis: verum

end;

A53: dom f1 c= dom f by FINSEQ_1:26;
then (X_axis f) . (len f1) = p2 `1 by A16, A17, A37, A38, GOBOARD1:def 1;
then A54: f /. (len f1) in rng (Line ((GoB f),(len (GoB f)))) by A53, A37, A40, GOBOARD2:16;

now :: thesis: for n being Nat st n in dom f1 holds
ex i, j being Nat st
( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) )

let n be Nat; :: thesis: ( n in dom f1 implies ex i, j being Nat st
( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) ) )
assume A55: n in dom f1 ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) )
dom f1 c= dom f by FINSEQ_1:26;
then consider i, j being Nat such that
A56: ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) by A55, GOBOARD2:14;
take i = i; :: thesis: ex j being Nat st
( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) )
take j = j; :: thesis: ( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) )
thus ( [i,j] in Indices (GoB f) & f1 /. n = (GoB f) * (i,j) ) by A55, A56, FINSEQ_4:68; :: thesis: verum

end;

then consider g1 being FinSequence of (TOP-REAL 2) such that
A57: ( g1 is_sequence_on GoB f & L~ g1 = L~ f1 & g1 /. 1 = f1 /. 1 & g1 /. (len g1) = f1 /. (len f1) ) and
A58: len f1 <= len g1 by A3, A5, GOBOARD2:12;

now :: thesis: for n being Nat st n in dom f2 holds
ex i, j being Nat st
( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) )

let n be Nat; :: thesis: ( n in dom f2 implies ex i, j being Nat st
( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) ) )
assume A59: n in dom f2 ; :: thesis: ex i, j being Nat st
( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) )
then (len f1) + n in dom f by FINSEQ_1:28;
then consider i, j being Nat such that
A60: ( [i,j] in Indices (GoB f) & f /. ((len f1) + n) = (GoB f) * (i,j) ) by GOBOARD2:14;
take i = i; :: thesis: ex j being Nat st
( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) )
take j = j; :: thesis: ( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) )
thus ( [i,j] in Indices (GoB f) & f2 /. n = (GoB f) * (i,j) ) by A59, A60, FINSEQ_4:69; :: thesis: verum

end;

then consider g2 being FinSequence of (TOP-REAL 2) such that
A61: ( g2 is_sequence_on GoB f & L~ g2 = L~ f2 & g2 /. 1 = f2 /. 1 & g2 /. (len g2) = f2 /. (len f2) ) and
A62: len f2 <= len g2 by A4, A6, GOBOARD2:12;
A63: 2 <= len g2 by A2, A62, XXREAL_0:2;
A64: 1 <= len f2 by A2, XXREAL_0:2;
then A65: 1 in dom f2 by FINSEQ_3:25;
then A66: f /. ((len f1) + 1) = f2 /. 1 by FINSEQ_4:69;
A67: ( Seg (len (Y_axis f)) = dom (Y_axis f) & len (Y_axis f) = len f ) by FINSEQ_1:def 3, GOBOARD1:def 2;
A68: ( Seg (len (Y_axis f1)) = dom (Y_axis f1) & len (Y_axis f1) = len f1 ) by FINSEQ_1:def 3, GOBOARD1:def 2;
A69: ( Seg (len (Y_axis f2)) = dom (Y_axis f2) & len (Y_axis f2) = len f2 ) by FINSEQ_1:def 3, GOBOARD1:def 2;
then A70: (Y_axis f2) . 1 = q1 `2 by A11, A65, GOBOARD1:def 2;

A71: now :: thesis: for m being Nat st m in dom f holds
q1 `2 <= (Y_axis f) . m

let m be Nat; :: thesis: ( m in dom f implies q1 `2 <= (Y_axis f) . m )
set s = (Y_axis f) . m;
assume A72: m in dom f ; :: thesis: q1 `2 <= (Y_axis f) . m
then A73: m <= len f by FINSEQ_3:25;
A74: 1 <= m by A72, FINSEQ_3:25;

now :: thesis: q1 `2 <= (Y_axis f) . m

per cases ( m <= len f1 or len f1 < m ) ;

suppose A75: m <= len f1 ; :: thesis: q1 `2 <= (Y_axis f) . m

reconsider u = f1 /. m as Point of (TOP-REAL 2) ;
A76: m in dom f1 by A74, A75, FINSEQ_3:25;
then f /. m = u by FINSEQ_4:68;
then A77: (Y_axis f) . m = u `2 by A16, A67, A72, GOBOARD1:def 2;
(Y_axis f1) . m = u `2 by A12, A68, A76, GOBOARD1:def 2;
hence q1 `2 <= (Y_axis f) . m by A9, A12, A68, A70, A76, A77; :: thesis: verum

end;

suppose A78: len f1 < m ; :: thesis: q1 `2 <= (Y_axis f) . m

then reconsider w5 = m - (len f1) as Element of NAT by INT_1:5;
w5 > 0 by A78, XREAL_1:50;
then A79: 1 <= w5 by NAT_1:14;
A80: m = w5 + (len f1) ;
then reconsider m1 = m - (len f1) as Nat ;
reconsider u = f2 /. m1 as Point of (TOP-REAL 2) ;
A81: w5 <= len f2 by A19, A73, A80, XREAL_1:6;
then f /. m = f2 /. w5 by A80, A79, SEQ_4:136;
then A82: (Y_axis f) . m = u `2 by A16, A67, A72, GOBOARD1:def 2;
A83: m1 in dom f2 by A79, A81, FINSEQ_3:25;
then (Y_axis f2) . m1 = u `2 by A11, A69, GOBOARD1:def 2;
hence q1 `2 <= (Y_axis f) . m by A10, A11, A69, A70, A83, A82; :: thesis: verum

end;

end;

end;

hence q1 `2 <= (Y_axis f) . m ; :: thesis: verum

end;

A84: (len f1) + 1 in dom f by A65, FINSEQ_1:28;
then (Y_axis f) . ((len f1) + 1) = q1 `2 by A16, A67, A66, GOBOARD1:def 2;
then A85: f /. ((len f1) + 1) in rng (Col ((GoB f),1)) by A84, A71, GOBOARD2:17;
A86: len f2 in dom f2 by A64, FINSEQ_3:25;
then A87: f /. ((len f1) + (len f2)) = f2 /. (len f2) by FINSEQ_4:69;
A88: (Y_axis f2) . (len f2) = q2 `2 by A11, A69, A86, GOBOARD1:def 2;

A89: now :: thesis: for m being Nat st m in dom f holds
(Y_axis f) . m <= q2 `2

let m be Nat; :: thesis: ( m in dom f implies (Y_axis f) . m <= q2 `2 )
set s = (Y_axis f) . m;
assume A90: m in dom f ; :: thesis: (Y_axis f) . m <= q2 `2
then A91: m <= len f by FINSEQ_3:25;
A92: 1 <= m by A90, FINSEQ_3:25;

now :: thesis: (Y_axis f) . m <= q2 `2

per cases ( m <= len f1 or len f1 < m ) ;

suppose A93: m <= len f1 ; :: thesis: (Y_axis f) . m <= q2 `2

reconsider u = f1 /. m as Point of (TOP-REAL 2) ;
A94: m in dom f1 by A92, A93, FINSEQ_3:25;
then f /. m = u by FINSEQ_4:68;
then A95: (Y_axis f) . m = u `2 by A16, A67, A90, GOBOARD1:def 2;
(Y_axis f1) . m = u `2 by A12, A68, A94, GOBOARD1:def 2;
hence (Y_axis f) . m <= q2 `2 by A9, A12, A68, A88, A94, A95; :: thesis: verum

end;

suppose A96: len f1 < m ; :: thesis: (Y_axis f) . m <= q2 `2

then reconsider w5 = m - (len f1) as Element of NAT by INT_1:5;
w5 > 0 by A96, XREAL_1:50;
then A97: 1 <= w5 by NAT_1:14;
A98: m = w5 + (len f1) ;
then reconsider m1 = m - (len f1) as Nat ;
reconsider u = f2 /. m1 as Point of (TOP-REAL 2) ;
A99: w5 <= len f2 by A19, A91, A98, XREAL_1:6;
then f /. m = f2 /. w5 by A98, A97, SEQ_4:136;
then A100: (Y_axis f) . m = u `2 by A16, A67, A90, GOBOARD1:def 2;
A101: m1 in dom f2 by A97, A99, FINSEQ_3:25;
then (Y_axis f2) . m1 = u `2 by A11, A69, GOBOARD1:def 2;
hence (Y_axis f) . m <= q2 `2 by A10, A11, A69, A88, A101, A100; :: thesis: verum

end;

end;

end;

hence (Y_axis f) . m <= q2 `2 ; :: thesis: verum

end;

A102: (len f1) + (len f2) in dom f by A86, FINSEQ_1:28;
then (Y_axis f) . ((len f1) + (len f2)) = q2 `2 by A16, A67, A87, GOBOARD1:def 2;
then A103: f /. ((len f1) + (len f2)) in rng (Col ((GoB f),(width (GoB f)))) by A102, A89, GOBOARD2:18;
2 <= len g1 by A1, A58, XXREAL_0:2;
hence L~ f1 meets L~ f2 by A57, A61, A15, A38, A66, A87, A36, A54, A85, A103, A63, Th2; :: thesis: verum