let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: ( f1 is special & f2 is special & 2 <= len f1 & 2 <= len f2 & f1 . 1 <> f1 . (len f1) & f2 . 1 <> f2 . (len f2) & 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: f1 is special and

A2: f2 is special and

A3: 2 <= len f1 and

A4: 2 <= len f2 and

A5: f1 . 1 <> f1 . (len f1) and

A6: f2 . 1 <> f2 . (len f2) 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

consider g1 being FinSequence of (TOP-REAL 2) such that

A11: 2 <= len g1 and

A12: g1 is special and

A13: g1 is one-to-one and

A14: L~ g1 c= L~ f1 and

A15: f1 . 1 = g1 . 1 and

A16: f1 . (len f1) = g1 . (len g1) and

A17: rng g1 c= rng f1 by A1, A3, A5, Th25;

consider g2 being FinSequence of (TOP-REAL 2) such that

A18: 2 <= len g2 and

A19: g2 is special and

A20: g2 is one-to-one and

A21: L~ g2 c= L~ f2 and

A22: f2 . 1 = g2 . 1 and

A23: f2 . (len f2) = g2 . (len g2) and

A24: rng g2 c= rng f2 by A2, A4, A6, Th25;

A25: for k being Nat st k in dom g2 & k + 1 in dom g2 holds

g2 /. k <> g2 /. (k + 1)

( (Y_axis g2) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis g2) . (len g2) )

for i being Nat st i in dom (X_axis g2) holds

( (X_axis g1) . 1 <= (X_axis g2) . i & (X_axis g2) . i <= (X_axis g1) . (len g1) )

for i being Nat st i in dom (Y_axis g2) holds

( (Y_axis g2) . 1 <= (Y_axis g2) . i & (Y_axis g2) . i <= (Y_axis g2) . (len g2) )

for i being Nat st i in dom (X_axis g1) holds

( (X_axis g1) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis g1) . (len g1) )

for k being Nat st k in dom g1 & k + 1 in dom g1 holds

g1 /. k <> g1 /. (k + 1)

then (L~ g1) /\ (L~ g2) <> {} ;

then (L~ f1) /\ (L~ f2) <> {} by A14, A21, XBOOLE_1:3, XBOOLE_1:27;

hence L~ f1 meets L~ f2 ; :: thesis: verum

assume that

A1: f1 is special and

A2: f2 is special and

A3: 2 <= len f1 and

A4: 2 <= len f2 and

A5: f1 . 1 <> f1 . (len f1) and

A6: f2 . 1 <> f2 . (len f2) 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

consider g1 being FinSequence of (TOP-REAL 2) such that

A11: 2 <= len g1 and

A12: g1 is special and

A13: g1 is one-to-one and

A14: L~ g1 c= L~ f1 and

A15: f1 . 1 = g1 . 1 and

A16: f1 . (len f1) = g1 . (len g1) and

A17: rng g1 c= rng f1 by A1, A3, A5, Th25;

consider g2 being FinSequence of (TOP-REAL 2) such that

A18: 2 <= len g2 and

A19: g2 is special and

A20: g2 is one-to-one and

A21: L~ g2 c= L~ f2 and

A22: f2 . 1 = g2 . 1 and

A23: f2 . (len f2) = g2 . (len g2) and

A24: rng g2 c= rng f2 by A2, A4, A6, Th25;

A25: for k being Nat st k in dom g2 & k + 1 in dom g2 holds

g2 /. k <> g2 /. (k + 1)

proof

for i being Nat st i in dom (Y_axis g1) holds
let k be Nat; :: thesis: ( k in dom g2 & k + 1 in dom g2 implies g2 /. k <> g2 /. (k + 1) )

assume that

A26: k in dom g2 and

A27: k + 1 in dom g2 ; :: thesis: g2 /. k <> g2 /. (k + 1)

A28: g2 . k = g2 /. k by A26, PARTFUN1:def 6;

k < k + 1 by NAT_1:13;

then g2 . k <> g2 . (k + 1) by A20, A26, A27;

hence g2 /. k <> g2 /. (k + 1) by A27, A28, PARTFUN1:def 6; :: thesis: verum

end;assume that

A26: k in dom g2 and

A27: k + 1 in dom g2 ; :: thesis: g2 /. k <> g2 /. (k + 1)

A28: g2 . k = g2 /. k by A26, PARTFUN1:def 6;

k < k + 1 by NAT_1:13;

then g2 . k <> g2 . (k + 1) by A20, A26, A27;

hence g2 /. k <> g2 /. (k + 1) by A27, A28, PARTFUN1:def 6; :: thesis: verum

( (Y_axis g2) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis g2) . (len g2) )

proof

then A48:
Y_axis g1 lies_between (Y_axis g2) . 1,(Y_axis g2) . (len g2)
by GOBOARD4:def 2;
let i be Nat; :: thesis: ( i in dom (Y_axis g1) implies ( (Y_axis g2) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis g2) . (len g2) ) )

A29: len (Y_axis f2) = len f2 by GOBOARD1:def 2;

A30: 1 <= len f2 by A4, XXREAL_0:2;

then 1 in Seg (len f2) by FINSEQ_1:1;

then A31: 1 in dom (Y_axis f2) by A29, FINSEQ_1:def 3;

len f2 in Seg (len f2) by A30, FINSEQ_1:1;

then A32: len f2 in dom (Y_axis f2) by A29, FINSEQ_1:def 3;

A33: len (Y_axis g2) = len g2 by GOBOARD1:def 2;

A34: 1 <= len g2 by A18, XXREAL_0:2;

then 1 in Seg (len g2) by FINSEQ_1:1;

then A35: 1 in dom (Y_axis g2) by A33, FINSEQ_1:def 3;

g2 /. 1 = g2 . 1 by A34, FINSEQ_4:15;

then A36: g2 /. 1 = f2 /. 1 by A22, A30, FINSEQ_4:15;

len g2 in Seg (len g2) by A34, FINSEQ_1:1;

then A37: len g2 in dom (Y_axis g2) by A33, FINSEQ_1:def 3;

g2 /. (len g2) = g2 . (len g2) by A34, FINSEQ_4:15;

then A38: g2 /. (len g2) = f2 /. (len f2) by A23, A30, FINSEQ_4:15;

assume A39: i in dom (Y_axis g1) ; :: thesis: ( (Y_axis g2) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis g2) . (len g2) )

then A40: (Y_axis g1) . i = (g1 /. i) `2 by GOBOARD1:def 2;

len (Y_axis g1) = len g1 by GOBOARD1:def 2;

then i in Seg (len g1) by A39, FINSEQ_1:def 3;

then A41: i in dom g1 by FINSEQ_1:def 3;

then g1 . i in rng g1 by FUNCT_1:def 3;

then consider y being object such that

A42: y in dom f1 and

A43: g1 . i = f1 . y by A17, FUNCT_1:def 3;

reconsider j = y as Element of NAT by A42;

f1 . j = f1 /. j by A42, PARTFUN1:def 6;

then A44: g1 /. i = f1 /. j by A41, A43, PARTFUN1:def 6;

( len (Y_axis f1) = len f1 & j in Seg (len f1) ) by A42, FINSEQ_1:def 3, GOBOARD1:def 2;

then A45: j in dom (Y_axis f1) by FINSEQ_1:def 3;

then A46: (Y_axis f1) . j = (f1 /. j) `2 by GOBOARD1:def 2;

(Y_axis f1) . j <= (Y_axis f2) . (len f2) by A9, A45, GOBOARD4:def 2;

then A47: (g1 /. i) `2 <= (g2 /. (len g2)) `2 by A38, A44, A46, A32, GOBOARD1:def 2;

(Y_axis f2) . 1 <= (Y_axis f1) . j by A9, A45, GOBOARD4:def 2;

then (g2 /. 1) `2 <= (g1 /. i) `2 by A36, A31, A44, A46, GOBOARD1:def 2;

hence ( (Y_axis g2) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis g2) . (len g2) ) by A35, A47, A40, A37, GOBOARD1:def 2; :: thesis: verum

end;A29: len (Y_axis f2) = len f2 by GOBOARD1:def 2;

A30: 1 <= len f2 by A4, XXREAL_0:2;

then 1 in Seg (len f2) by FINSEQ_1:1;

then A31: 1 in dom (Y_axis f2) by A29, FINSEQ_1:def 3;

len f2 in Seg (len f2) by A30, FINSEQ_1:1;

then A32: len f2 in dom (Y_axis f2) by A29, FINSEQ_1:def 3;

A33: len (Y_axis g2) = len g2 by GOBOARD1:def 2;

A34: 1 <= len g2 by A18, XXREAL_0:2;

then 1 in Seg (len g2) by FINSEQ_1:1;

then A35: 1 in dom (Y_axis g2) by A33, FINSEQ_1:def 3;

g2 /. 1 = g2 . 1 by A34, FINSEQ_4:15;

then A36: g2 /. 1 = f2 /. 1 by A22, A30, FINSEQ_4:15;

len g2 in Seg (len g2) by A34, FINSEQ_1:1;

then A37: len g2 in dom (Y_axis g2) by A33, FINSEQ_1:def 3;

g2 /. (len g2) = g2 . (len g2) by A34, FINSEQ_4:15;

then A38: g2 /. (len g2) = f2 /. (len f2) by A23, A30, FINSEQ_4:15;

assume A39: i in dom (Y_axis g1) ; :: thesis: ( (Y_axis g2) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis g2) . (len g2) )

then A40: (Y_axis g1) . i = (g1 /. i) `2 by GOBOARD1:def 2;

len (Y_axis g1) = len g1 by GOBOARD1:def 2;

then i in Seg (len g1) by A39, FINSEQ_1:def 3;

then A41: i in dom g1 by FINSEQ_1:def 3;

then g1 . i in rng g1 by FUNCT_1:def 3;

then consider y being object such that

A42: y in dom f1 and

A43: g1 . i = f1 . y by A17, FUNCT_1:def 3;

reconsider j = y as Element of NAT by A42;

f1 . j = f1 /. j by A42, PARTFUN1:def 6;

then A44: g1 /. i = f1 /. j by A41, A43, PARTFUN1:def 6;

( len (Y_axis f1) = len f1 & j in Seg (len f1) ) by A42, FINSEQ_1:def 3, GOBOARD1:def 2;

then A45: j in dom (Y_axis f1) by FINSEQ_1:def 3;

then A46: (Y_axis f1) . j = (f1 /. j) `2 by GOBOARD1:def 2;

(Y_axis f1) . j <= (Y_axis f2) . (len f2) by A9, A45, GOBOARD4:def 2;

then A47: (g1 /. i) `2 <= (g2 /. (len g2)) `2 by A38, A44, A46, A32, GOBOARD1:def 2;

(Y_axis f2) . 1 <= (Y_axis f1) . j by A9, A45, GOBOARD4:def 2;

then (g2 /. 1) `2 <= (g1 /. i) `2 by A36, A31, A44, A46, GOBOARD1:def 2;

hence ( (Y_axis g2) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis g2) . (len g2) ) by A35, A47, A40, A37, GOBOARD1:def 2; :: thesis: verum

for i being Nat st i in dom (X_axis g2) holds

( (X_axis g1) . 1 <= (X_axis g2) . i & (X_axis g2) . i <= (X_axis g1) . (len g1) )

proof

then A68:
X_axis g2 lies_between (X_axis g1) . 1,(X_axis g1) . (len g1)
by GOBOARD4:def 2;
let i be Nat; :: thesis: ( i in dom (X_axis g2) implies ( (X_axis g1) . 1 <= (X_axis g2) . i & (X_axis g2) . i <= (X_axis g1) . (len g1) ) )

A49: len (X_axis f1) = len f1 by GOBOARD1:def 1;

A50: 1 <= len f1 by A3, XXREAL_0:2;

then 1 in Seg (len f1) by FINSEQ_1:1;

then A51: 1 in dom (X_axis f1) by A49, FINSEQ_1:def 3;

len f1 in Seg (len f1) by A50, FINSEQ_1:1;

then A52: len f1 in dom (X_axis f1) by A49, FINSEQ_1:def 3;

A53: len (X_axis g1) = len g1 by GOBOARD1:def 1;

A54: 1 <= len g1 by A11, XXREAL_0:2;

then 1 in Seg (len g1) by FINSEQ_1:1;

then A55: 1 in dom (X_axis g1) by A53, FINSEQ_1:def 3;

g1 /. 1 = g1 . 1 by A54, FINSEQ_4:15;

then A56: g1 /. 1 = f1 /. 1 by A15, A50, FINSEQ_4:15;

len g1 in Seg (len g1) by A54, FINSEQ_1:1;

then A57: len g1 in dom (X_axis g1) by A53, FINSEQ_1:def 3;

g1 /. (len g1) = g1 . (len g1) by A54, FINSEQ_4:15;

then A58: g1 /. (len g1) = f1 /. (len f1) by A16, A50, FINSEQ_4:15;

assume A59: i in dom (X_axis g2) ; :: thesis: ( (X_axis g1) . 1 <= (X_axis g2) . i & (X_axis g2) . i <= (X_axis g1) . (len g1) )

then A60: (X_axis g2) . i = (g2 /. i) `1 by GOBOARD1:def 1;

len (X_axis g2) = len g2 by GOBOARD1:def 1;

then i in Seg (len g2) by A59, FINSEQ_1:def 3;

then A61: i in dom g2 by FINSEQ_1:def 3;

then g2 . i in rng g2 by FUNCT_1:def 3;

then consider y being object such that

A62: y in dom f2 and

A63: g2 . i = f2 . y by A24, FUNCT_1:def 3;

reconsider j = y as Element of NAT by A62;

f2 . j = f2 /. j by A62, PARTFUN1:def 6;

then A64: g2 /. i = f2 /. j by A61, A63, PARTFUN1:def 6;

( len (X_axis f2) = len f2 & j in Seg (len f2) ) by A62, FINSEQ_1:def 3, GOBOARD1:def 1;

then A65: j in dom (X_axis f2) by FINSEQ_1:def 3;

then A66: (X_axis f2) . j = (f2 /. j) `1 by GOBOARD1:def 1;

(X_axis f2) . j <= (X_axis f1) . (len f1) by A8, A65, GOBOARD4:def 2;

then A67: (g2 /. i) `1 <= (g1 /. (len g1)) `1 by A58, A64, A66, A52, GOBOARD1:def 1;

(X_axis f1) . 1 <= (X_axis f2) . j by A8, A65, GOBOARD4:def 2;

then (g1 /. 1) `1 <= (g2 /. i) `1 by A56, A51, A64, A66, GOBOARD1:def 1;

hence ( (X_axis g1) . 1 <= (X_axis g2) . i & (X_axis g2) . i <= (X_axis g1) . (len g1) ) by A55, A67, A60, A57, GOBOARD1:def 1; :: thesis: verum

end;A49: len (X_axis f1) = len f1 by GOBOARD1:def 1;

A50: 1 <= len f1 by A3, XXREAL_0:2;

then 1 in Seg (len f1) by FINSEQ_1:1;

then A51: 1 in dom (X_axis f1) by A49, FINSEQ_1:def 3;

len f1 in Seg (len f1) by A50, FINSEQ_1:1;

then A52: len f1 in dom (X_axis f1) by A49, FINSEQ_1:def 3;

A53: len (X_axis g1) = len g1 by GOBOARD1:def 1;

A54: 1 <= len g1 by A11, XXREAL_0:2;

then 1 in Seg (len g1) by FINSEQ_1:1;

then A55: 1 in dom (X_axis g1) by A53, FINSEQ_1:def 3;

g1 /. 1 = g1 . 1 by A54, FINSEQ_4:15;

then A56: g1 /. 1 = f1 /. 1 by A15, A50, FINSEQ_4:15;

len g1 in Seg (len g1) by A54, FINSEQ_1:1;

then A57: len g1 in dom (X_axis g1) by A53, FINSEQ_1:def 3;

g1 /. (len g1) = g1 . (len g1) by A54, FINSEQ_4:15;

then A58: g1 /. (len g1) = f1 /. (len f1) by A16, A50, FINSEQ_4:15;

assume A59: i in dom (X_axis g2) ; :: thesis: ( (X_axis g1) . 1 <= (X_axis g2) . i & (X_axis g2) . i <= (X_axis g1) . (len g1) )

then A60: (X_axis g2) . i = (g2 /. i) `1 by GOBOARD1:def 1;

len (X_axis g2) = len g2 by GOBOARD1:def 1;

then i in Seg (len g2) by A59, FINSEQ_1:def 3;

then A61: i in dom g2 by FINSEQ_1:def 3;

then g2 . i in rng g2 by FUNCT_1:def 3;

then consider y being object such that

A62: y in dom f2 and

A63: g2 . i = f2 . y by A24, FUNCT_1:def 3;

reconsider j = y as Element of NAT by A62;

f2 . j = f2 /. j by A62, PARTFUN1:def 6;

then A64: g2 /. i = f2 /. j by A61, A63, PARTFUN1:def 6;

( len (X_axis f2) = len f2 & j in Seg (len f2) ) by A62, FINSEQ_1:def 3, GOBOARD1:def 1;

then A65: j in dom (X_axis f2) by FINSEQ_1:def 3;

then A66: (X_axis f2) . j = (f2 /. j) `1 by GOBOARD1:def 1;

(X_axis f2) . j <= (X_axis f1) . (len f1) by A8, A65, GOBOARD4:def 2;

then A67: (g2 /. i) `1 <= (g1 /. (len g1)) `1 by A58, A64, A66, A52, GOBOARD1:def 1;

(X_axis f1) . 1 <= (X_axis f2) . j by A8, A65, GOBOARD4:def 2;

then (g1 /. 1) `1 <= (g2 /. i) `1 by A56, A51, A64, A66, GOBOARD1:def 1;

hence ( (X_axis g1) . 1 <= (X_axis g2) . i & (X_axis g2) . i <= (X_axis g1) . (len g1) ) by A55, A67, A60, A57, GOBOARD1:def 1; :: thesis: verum

for i being Nat st i in dom (Y_axis g2) holds

( (Y_axis g2) . 1 <= (Y_axis g2) . i & (Y_axis g2) . i <= (Y_axis g2) . (len g2) )

proof

then A88:
Y_axis g2 lies_between (Y_axis g2) . 1,(Y_axis g2) . (len g2)
by GOBOARD4:def 2;
let i be Nat; :: thesis: ( i in dom (Y_axis g2) implies ( (Y_axis g2) . 1 <= (Y_axis g2) . i & (Y_axis g2) . i <= (Y_axis g2) . (len g2) ) )

A69: len (Y_axis f2) = len f2 by GOBOARD1:def 2;

A70: 1 <= len f2 by A4, XXREAL_0:2;

then 1 in Seg (len f2) by FINSEQ_1:1;

then A71: 1 in dom (Y_axis f2) by A69, FINSEQ_1:def 3;

A72: 1 <= len g2 by A18, XXREAL_0:2;

then g2 /. 1 = g2 . 1 by FINSEQ_4:15;

then A73: g2 /. 1 = f2 /. 1 by A22, A70, FINSEQ_4:15;

A74: len (Y_axis g2) = len g2 by GOBOARD1:def 2;

then len g2 in Seg (len (Y_axis g2)) by A72, FINSEQ_1:1;

then A75: len g2 in dom (Y_axis g2) by FINSEQ_1:def 3;

g2 /. (len g2) = g2 . (len g2) by A72, FINSEQ_4:15;

then A76: g2 /. (len g2) = f2 /. (len f2) by A23, A70, FINSEQ_4:15;

1 in Seg (len g2) by A72, FINSEQ_1:1;

then A77: 1 in dom (Y_axis g2) by A74, FINSEQ_1:def 3;

len f2 in Seg (len f2) by A70, FINSEQ_1:1;

then A78: len f2 in dom (Y_axis f2) by A69, FINSEQ_1:def 3;

assume A79: i in dom (Y_axis g2) ; :: thesis: ( (Y_axis g2) . 1 <= (Y_axis g2) . i & (Y_axis g2) . i <= (Y_axis g2) . (len g2) )

then A80: (Y_axis g2) . i = (g2 /. i) `2 by GOBOARD1:def 2;

i in Seg (len g2) by A79, A74, FINSEQ_1:def 3;

then A81: i in dom g2 by FINSEQ_1:def 3;

then g2 . i in rng g2 by FUNCT_1:def 3;

then consider y being object such that

A82: y in dom f2 and

A83: g2 . i = f2 . y by A24, FUNCT_1:def 3;

reconsider j = y as Element of NAT by A82;

f2 . j = f2 /. j by A82, PARTFUN1:def 6;

then A84: g2 /. i = f2 /. j by A81, A83, PARTFUN1:def 6;

j in Seg (len f2) by A82, FINSEQ_1:def 3;

then A85: j in dom (Y_axis f2) by A69, FINSEQ_1:def 3;

then A86: (Y_axis f2) . j = (f2 /. j) `2 by GOBOARD1:def 2;

(Y_axis f2) . j <= (Y_axis f2) . (len f2) by A10, A85, GOBOARD4:def 2;

then A87: (g2 /. i) `2 <= (g2 /. (len g2)) `2 by A76, A84, A86, A78, GOBOARD1:def 2;

(Y_axis f2) . 1 <= (Y_axis f2) . j by A10, A85, GOBOARD4:def 2;

then (g2 /. 1) `2 <= (g2 /. i) `2 by A73, A71, A84, A86, GOBOARD1:def 2;

hence ( (Y_axis g2) . 1 <= (Y_axis g2) . i & (Y_axis g2) . i <= (Y_axis g2) . (len g2) ) by A77, A87, A80, A75, GOBOARD1:def 2; :: thesis: verum

end;A69: len (Y_axis f2) = len f2 by GOBOARD1:def 2;

A70: 1 <= len f2 by A4, XXREAL_0:2;

then 1 in Seg (len f2) by FINSEQ_1:1;

then A71: 1 in dom (Y_axis f2) by A69, FINSEQ_1:def 3;

A72: 1 <= len g2 by A18, XXREAL_0:2;

then g2 /. 1 = g2 . 1 by FINSEQ_4:15;

then A73: g2 /. 1 = f2 /. 1 by A22, A70, FINSEQ_4:15;

A74: len (Y_axis g2) = len g2 by GOBOARD1:def 2;

then len g2 in Seg (len (Y_axis g2)) by A72, FINSEQ_1:1;

then A75: len g2 in dom (Y_axis g2) by FINSEQ_1:def 3;

g2 /. (len g2) = g2 . (len g2) by A72, FINSEQ_4:15;

then A76: g2 /. (len g2) = f2 /. (len f2) by A23, A70, FINSEQ_4:15;

1 in Seg (len g2) by A72, FINSEQ_1:1;

then A77: 1 in dom (Y_axis g2) by A74, FINSEQ_1:def 3;

len f2 in Seg (len f2) by A70, FINSEQ_1:1;

then A78: len f2 in dom (Y_axis f2) by A69, FINSEQ_1:def 3;

assume A79: i in dom (Y_axis g2) ; :: thesis: ( (Y_axis g2) . 1 <= (Y_axis g2) . i & (Y_axis g2) . i <= (Y_axis g2) . (len g2) )

then A80: (Y_axis g2) . i = (g2 /. i) `2 by GOBOARD1:def 2;

i in Seg (len g2) by A79, A74, FINSEQ_1:def 3;

then A81: i in dom g2 by FINSEQ_1:def 3;

then g2 . i in rng g2 by FUNCT_1:def 3;

then consider y being object such that

A82: y in dom f2 and

A83: g2 . i = f2 . y by A24, FUNCT_1:def 3;

reconsider j = y as Element of NAT by A82;

f2 . j = f2 /. j by A82, PARTFUN1:def 6;

then A84: g2 /. i = f2 /. j by A81, A83, PARTFUN1:def 6;

j in Seg (len f2) by A82, FINSEQ_1:def 3;

then A85: j in dom (Y_axis f2) by A69, FINSEQ_1:def 3;

then A86: (Y_axis f2) . j = (f2 /. j) `2 by GOBOARD1:def 2;

(Y_axis f2) . j <= (Y_axis f2) . (len f2) by A10, A85, GOBOARD4:def 2;

then A87: (g2 /. i) `2 <= (g2 /. (len g2)) `2 by A76, A84, A86, A78, GOBOARD1:def 2;

(Y_axis f2) . 1 <= (Y_axis f2) . j by A10, A85, GOBOARD4:def 2;

then (g2 /. 1) `2 <= (g2 /. i) `2 by A73, A71, A84, A86, GOBOARD1:def 2;

hence ( (Y_axis g2) . 1 <= (Y_axis g2) . i & (Y_axis g2) . i <= (Y_axis g2) . (len g2) ) by A77, A87, A80, A75, GOBOARD1:def 2; :: thesis: verum

for i being Nat st i in dom (X_axis g1) holds

( (X_axis g1) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis g1) . (len g1) )

proof

then A108:
X_axis g1 lies_between (X_axis g1) . 1,(X_axis g1) . (len g1)
by GOBOARD4:def 2;
let i be Nat; :: thesis: ( i in dom (X_axis g1) implies ( (X_axis g1) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis g1) . (len g1) ) )

A89: len (X_axis f1) = len f1 by GOBOARD1:def 1;

assume A90: i in dom (X_axis g1) ; :: thesis: ( (X_axis g1) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis g1) . (len g1) )

then A91: (X_axis g1) . i = (g1 /. i) `1 by GOBOARD1:def 1;

A92: 1 <= len f1 by A3, XXREAL_0:2;

then len f1 in Seg (len f1) by FINSEQ_1:1;

then A93: len f1 in dom (X_axis f1) by A89, FINSEQ_1:def 3;

A94: 1 <= len g1 by A11, XXREAL_0:2;

then g1 /. 1 = g1 . 1 by FINSEQ_4:15;

then A95: g1 /. 1 = f1 /. 1 by A15, A92, FINSEQ_4:15;

g1 /. (len g1) = g1 . (len g1) by A94, FINSEQ_4:15;

then A96: g1 /. (len g1) = f1 /. (len f1) by A16, A92, FINSEQ_4:15;

A97: len (X_axis g1) = len g1 by GOBOARD1:def 1;

then A98: 1 in dom (X_axis g1) by A94, FINSEQ_3:25;

i in Seg (len g1) by A90, A97, FINSEQ_1:def 3;

then A99: i in dom g1 by FINSEQ_1:def 3;

then g1 . i in rng g1 by FUNCT_1:def 3;

then consider y being object such that

A100: y in dom f1 and

A101: g1 . i = f1 . y by A17, FUNCT_1:def 3;

reconsider j = y as Element of NAT by A100;

f1 . j = f1 /. j by A100, PARTFUN1:def 6;

then A102: g1 /. i = f1 /. j by A99, A101, PARTFUN1:def 6;

len g1 in Seg (len g1) by A94, FINSEQ_1:1;

then A103: len g1 in dom (X_axis g1) by A97, FINSEQ_1:def 3;

j in Seg (len f1) by A100, FINSEQ_1:def 3;

then A104: j in dom (X_axis f1) by A89, FINSEQ_1:def 3;

then A105: (X_axis f1) . j = (f1 /. j) `1 by GOBOARD1:def 1;

(X_axis f1) . j <= (X_axis f1) . (len f1) by A7, A104, GOBOARD4:def 2;

then A106: (g1 /. i) `1 <= (g1 /. (len g1)) `1 by A96, A102, A105, A93, GOBOARD1:def 1;

A107: (X_axis f1) . 1 <= (X_axis f1) . j by A7, A104, GOBOARD4:def 2;

1 in dom (X_axis f1) by A89, A92, FINSEQ_3:25;

then (g1 /. 1) `1 <= (g1 /. i) `1 by A95, A102, A107, A105, GOBOARD1:def 1;

hence ( (X_axis g1) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis g1) . (len g1) ) by A98, A106, A91, A103, GOBOARD1:def 1; :: thesis: verum

end;A89: len (X_axis f1) = len f1 by GOBOARD1:def 1;

assume A90: i in dom (X_axis g1) ; :: thesis: ( (X_axis g1) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis g1) . (len g1) )

then A91: (X_axis g1) . i = (g1 /. i) `1 by GOBOARD1:def 1;

A92: 1 <= len f1 by A3, XXREAL_0:2;

then len f1 in Seg (len f1) by FINSEQ_1:1;

then A93: len f1 in dom (X_axis f1) by A89, FINSEQ_1:def 3;

A94: 1 <= len g1 by A11, XXREAL_0:2;

then g1 /. 1 = g1 . 1 by FINSEQ_4:15;

then A95: g1 /. 1 = f1 /. 1 by A15, A92, FINSEQ_4:15;

g1 /. (len g1) = g1 . (len g1) by A94, FINSEQ_4:15;

then A96: g1 /. (len g1) = f1 /. (len f1) by A16, A92, FINSEQ_4:15;

A97: len (X_axis g1) = len g1 by GOBOARD1:def 1;

then A98: 1 in dom (X_axis g1) by A94, FINSEQ_3:25;

i in Seg (len g1) by A90, A97, FINSEQ_1:def 3;

then A99: i in dom g1 by FINSEQ_1:def 3;

then g1 . i in rng g1 by FUNCT_1:def 3;

then consider y being object such that

A100: y in dom f1 and

A101: g1 . i = f1 . y by A17, FUNCT_1:def 3;

reconsider j = y as Element of NAT by A100;

f1 . j = f1 /. j by A100, PARTFUN1:def 6;

then A102: g1 /. i = f1 /. j by A99, A101, PARTFUN1:def 6;

len g1 in Seg (len g1) by A94, FINSEQ_1:1;

then A103: len g1 in dom (X_axis g1) by A97, FINSEQ_1:def 3;

j in Seg (len f1) by A100, FINSEQ_1:def 3;

then A104: j in dom (X_axis f1) by A89, FINSEQ_1:def 3;

then A105: (X_axis f1) . j = (f1 /. j) `1 by GOBOARD1:def 1;

(X_axis f1) . j <= (X_axis f1) . (len f1) by A7, A104, GOBOARD4:def 2;

then A106: (g1 /. i) `1 <= (g1 /. (len g1)) `1 by A96, A102, A105, A93, GOBOARD1:def 1;

A107: (X_axis f1) . 1 <= (X_axis f1) . j by A7, A104, GOBOARD4:def 2;

1 in dom (X_axis f1) by A89, A92, FINSEQ_3:25;

then (g1 /. 1) `1 <= (g1 /. i) `1 by A95, A102, A107, A105, GOBOARD1:def 1;

hence ( (X_axis g1) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis g1) . (len g1) ) by A98, A106, A91, A103, GOBOARD1:def 1; :: thesis: verum

for k being Nat st k in dom g1 & k + 1 in dom g1 holds

g1 /. k <> g1 /. (k + 1)

proof

then
L~ g1 meets L~ g2
by A11, A12, A18, A19, A108, A68, A48, A88, A25, GOBOARD4:4;
let k be Nat; :: thesis: ( k in dom g1 & k + 1 in dom g1 implies g1 /. k <> g1 /. (k + 1) )

assume that

A109: k in dom g1 and

A110: k + 1 in dom g1 ; :: thesis: g1 /. k <> g1 /. (k + 1)

A111: g1 . k = g1 /. k by A109, PARTFUN1:def 6;

k < k + 1 by NAT_1:13;

then g1 . k <> g1 . (k + 1) by A13, A109, A110;

hence g1 /. k <> g1 /. (k + 1) by A110, A111, PARTFUN1:def 6; :: thesis: verum

end;assume that

A109: k in dom g1 and

A110: k + 1 in dom g1 ; :: thesis: g1 /. k <> g1 /. (k + 1)

A111: g1 . k = g1 /. k by A109, PARTFUN1:def 6;

k < k + 1 by NAT_1:13;

then g1 . k <> g1 . (k + 1) by A13, A109, A110;

hence g1 /. k <> g1 /. (k + 1) by A110, A111, PARTFUN1:def 6; :: thesis: verum

then (L~ g1) /\ (L~ g2) <> {} ;

then (L~ f1) /\ (L~ f2) <> {} by A14, A21, XBOOLE_1:3, XBOOLE_1:27;

hence L~ f1 meets L~ f2 ; :: thesis: verum