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 A1:
( 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) )
; :: thesis: L~ f1 meets L~ f2
then consider g1 being FinSequence of (TOP-REAL 2) such that
A2:
( 2 <= len g1 & g1 is special & g1 is one-to-one & L~ g1 c= L~ f1 & f1 . 1 = g1 . 1 & f1 . (len f1) = g1 . (len g1) & rng g1 c= rng f1 )
by Th29;
consider g2 being FinSequence of (TOP-REAL 2) such that
A3:
( 2 <= len g2 & g2 is special & g2 is one-to-one & L~ g2 c= L~ f2 & f2 . 1 = g2 . 1 & f2 . (len f2) = g2 . (len g2) & rng g2 c= rng f2 )
by A1, Th29;
for i being Element of 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
let i be
Element of
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) ) )
assume A4:
i in dom (X_axis g1)
;
:: thesis: ( (X_axis g1) . 1 <= (X_axis g1) . i & (X_axis g1) . i <= (X_axis g1) . (len g1) )
A5:
(
len (X_axis f1) = len f1 & ( for
j being
Element of
NAT st
j in dom (X_axis f1) holds
(X_axis f1) . j = (f1 /. j) `1 ) )
by GOBOARD1:def 3;
A6:
(
len (X_axis g1) = len g1 & ( for
j being
Element of
NAT st
j in dom (X_axis g1) holds
(X_axis g1) . j = (g1 /. j) `1 ) )
by GOBOARD1:def 3;
A7:
1
<= len g1
by A2, XXREAL_0:2;
then A8:
1
in dom (X_axis g1)
by A6, FINSEQ_3:27;
A9:
g1 /. 1
= g1 . 1
by A7, FINSEQ_4:24;
A10:
1
<= len f1
by A1, XXREAL_0:2;
then A11:
g1 /. 1
= f1 /. 1
by A2, A9, FINSEQ_4:24;
g1 /. (len g1) = g1 . (len g1)
by A7, FINSEQ_4:24;
then A12:
g1 /. (len g1) = f1 /. (len f1)
by A2, A10, FINSEQ_4:24;
A13:
1
in dom (X_axis f1)
by A5, A10, FINSEQ_3:27;
i in Seg (len g1)
by A4, A6, FINSEQ_1:def 3;
then A14:
i in dom g1
by FINSEQ_1:def 3;
then
g1 . i in rng g1
by FUNCT_1:def 5;
then consider y being
set such that A15:
(
y in dom f1 &
g1 . i = f1 . y )
by A2, FUNCT_1:def 5;
reconsider j =
y as
Element of
NAT by A15;
f1 . j = f1 /. j
by A15, PARTFUN1:def 8;
then A16:
(
j in dom f1 &
g1 /. i = f1 /. j )
by A14, A15, PARTFUN1:def 8;
j in Seg (len f1)
by A15, FINSEQ_1:def 3;
then A17:
j in dom (X_axis f1)
by A5, FINSEQ_1:def 3;
then A18:
(
(X_axis f1) . 1
<= (X_axis f1) . j &
(X_axis f1) . j <= (X_axis f1) . (len f1) )
by A1, GOBOARD4:def 2;
A19:
(X_axis f1) . j = (f1 /. j) `1
by A17, GOBOARD1:def 3;
len f1 in Seg (len f1)
by A10, FINSEQ_1:3;
then
len f1 in dom (X_axis f1)
by A5, FINSEQ_1:def 3;
then A20:
(
(g1 /. 1) `1 <= (g1 /. i) `1 &
(g1 /. i) `1 <= (g1 /. (len g1)) `1 )
by A11, A12, A13, A16, A18, A19, GOBOARD1:def 3;
A21:
(X_axis g1) . i = (g1 /. i) `1
by A4, GOBOARD1:def 3;
len g1 in Seg (len g1)
by A7, FINSEQ_1:3;
then
len g1 in dom (X_axis g1)
by A6, FINSEQ_1:def 3;
hence
(
(X_axis g1) . 1
<= (X_axis g1) . i &
(X_axis g1) . i <= (X_axis g1) . (len g1) )
by A8, A20, A21, GOBOARD1:def 3;
:: thesis: verum
end;
then A22:
X_axis g1 lies_between (X_axis g1) . 1,(X_axis g1) . (len g1)
by GOBOARD4:def 2;
for i being Element of 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
let i be
Element of
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) ) )
assume A23:
i in dom (X_axis g2)
;
:: thesis: ( (X_axis g1) . 1 <= (X_axis g2) . i & (X_axis g2) . i <= (X_axis g1) . (len g1) )
A24:
(
len (X_axis f2) = len f2 & ( for
j being
Element of
NAT st
j in dom (X_axis f2) holds
(X_axis f2) . j = (f2 /. j) `1 ) )
by GOBOARD1:def 3;
A25:
(
len (X_axis f1) = len f1 & ( for
j being
Element of
NAT st
j in dom (X_axis f1) holds
(X_axis f1) . j = (f1 /. j) `1 ) )
by GOBOARD1:def 3;
A26:
(
len (X_axis g2) = len g2 & ( for
j being
Element of
NAT st
j in dom (X_axis g2) holds
(X_axis g2) . j = (g2 /. j) `1 ) )
by GOBOARD1:def 3;
A27:
(
len (X_axis g1) = len g1 & ( for
j being
Element of
NAT st
j in dom (X_axis g1) holds
(X_axis g1) . j = (g1 /. j) `1 ) )
by GOBOARD1:def 3;
A28:
1
<= len g1
by A2, XXREAL_0:2;
then
1
in Seg (len g1)
by FINSEQ_1:3;
then A29:
1
in dom (X_axis g1)
by A27, FINSEQ_1:def 3;
A30:
g1 /. 1
= g1 . 1
by A28, FINSEQ_4:24;
A31:
1
<= len f1
by A1, XXREAL_0:2;
then A32:
g1 /. 1
= f1 /. 1
by A2, A30, FINSEQ_4:24;
g1 /. (len g1) = g1 . (len g1)
by A28, FINSEQ_4:24;
then A33:
g1 /. (len g1) = f1 /. (len f1)
by A2, A31, FINSEQ_4:24;
1
in Seg (len f1)
by A31, FINSEQ_1:3;
then A34:
1
in dom (X_axis f1)
by A25, FINSEQ_1:def 3;
i in Seg (len g2)
by A23, A26, FINSEQ_1:def 3;
then A35:
i in dom g2
by FINSEQ_1:def 3;
then
g2 . i in rng g2
by FUNCT_1:def 5;
then consider y being
set such that A36:
(
y in dom f2 &
g2 . i = f2 . y )
by A3, FUNCT_1:def 5;
reconsider j =
y as
Element of
NAT by A36;
f2 . j = f2 /. j
by A36, PARTFUN1:def 8;
then A37:
(
j in dom f2 &
g2 /. i = f2 /. j )
by A35, A36, PARTFUN1:def 8;
j in Seg (len f2)
by A36, FINSEQ_1:def 3;
then A38:
j in dom (X_axis f2)
by A24, FINSEQ_1:def 3;
then A39:
(
(X_axis f1) . 1
<= (X_axis f2) . j &
(X_axis f2) . j <= (X_axis f1) . (len f1) )
by A1, GOBOARD4:def 2;
A40:
(X_axis f2) . j = (f2 /. j) `1
by A38, GOBOARD1:def 3;
len f1 in Seg (len f1)
by A31, FINSEQ_1:3;
then
len f1 in dom (X_axis f1)
by A25, FINSEQ_1:def 3;
then A41:
(
(g1 /. 1) `1 <= (g2 /. i) `1 &
(g2 /. i) `1 <= (g1 /. (len g1)) `1 )
by A32, A33, A34, A37, A39, A40, GOBOARD1:def 3;
A42:
(X_axis g2) . i = (g2 /. i) `1
by A23, GOBOARD1:def 3;
len g1 in Seg (len g1)
by A28, FINSEQ_1:3;
then
len g1 in dom (X_axis g1)
by A27, FINSEQ_1:def 3;
hence
(
(X_axis g1) . 1
<= (X_axis g2) . i &
(X_axis g2) . i <= (X_axis g1) . (len g1) )
by A29, A41, A42, GOBOARD1:def 3;
:: thesis: verum
end;
then A43:
X_axis g2 lies_between (X_axis g1) . 1,(X_axis g1) . (len g1)
by GOBOARD4:def 2;
for i being Element of NAT st i in dom (Y_axis g1) holds
( (Y_axis g2) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis g2) . (len g2) )
proof
let i be
Element of
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) ) )
assume A44:
i in dom (Y_axis g1)
;
:: thesis: ( (Y_axis g2) . 1 <= (Y_axis g1) . i & (Y_axis g1) . i <= (Y_axis g2) . (len g2) )
A45:
(
len (Y_axis f1) = len f1 & ( for
j being
Element of
NAT st
j in dom (Y_axis f1) holds
(Y_axis f1) . j = (f1 /. j) `2 ) )
by GOBOARD1:def 4;
A46:
(
len (Y_axis f2) = len f2 & ( for
j being
Element of
NAT st
j in dom (Y_axis f2) holds
(Y_axis f2) . j = (f2 /. j) `2 ) )
by GOBOARD1:def 4;
A47:
(
len (Y_axis g1) = len g1 & ( for
j being
Element of
NAT st
j in dom (Y_axis g1) holds
(Y_axis g1) . j = (g1 /. j) `2 ) )
by GOBOARD1:def 4;
A48:
(
len (Y_axis g2) = len g2 & ( for
j being
Element of
NAT st
j in dom (Y_axis g2) holds
(Y_axis g2) . j = (g2 /. j) `2 ) )
by GOBOARD1:def 4;
A49:
1
<= len g2
by A3, XXREAL_0:2;
then
1
in Seg (len g2)
by FINSEQ_1:3;
then A50:
1
in dom (Y_axis g2)
by A48, FINSEQ_1:def 3;
A51:
g2 /. 1
= g2 . 1
by A49, FINSEQ_4:24;
A52:
1
<= len f2
by A1, XXREAL_0:2;
then A53:
g2 /. 1
= f2 /. 1
by A3, A51, FINSEQ_4:24;
g2 /. (len g2) = g2 . (len g2)
by A49, FINSEQ_4:24;
then A54:
g2 /. (len g2) = f2 /. (len f2)
by A3, A52, FINSEQ_4:24;
1
in Seg (len f2)
by A52, FINSEQ_1:3;
then A55:
1
in dom (Y_axis f2)
by A46, FINSEQ_1:def 3;
i in Seg (len g1)
by A44, A47, FINSEQ_1:def 3;
then A56:
i in dom g1
by FINSEQ_1:def 3;
then
g1 . i in rng g1
by FUNCT_1:def 5;
then consider y being
set such that A57:
(
y in dom f1 &
g1 . i = f1 . y )
by A2, FUNCT_1:def 5;
reconsider j =
y as
Element of
NAT by A57;
f1 . j = f1 /. j
by A57, PARTFUN1:def 8;
then A58:
(
j in dom f1 &
g1 /. i = f1 /. j )
by A56, A57, PARTFUN1:def 8;
j in Seg (len f1)
by A57, FINSEQ_1:def 3;
then A59:
j in dom (Y_axis f1)
by A45, FINSEQ_1:def 3;
then A60:
(
(Y_axis f2) . 1
<= (Y_axis f1) . j &
(Y_axis f1) . j <= (Y_axis f2) . (len f2) )
by A1, GOBOARD4:def 2;
A61:
(Y_axis f1) . j = (f1 /. j) `2
by A59, GOBOARD1:def 4;
len f2 in Seg (len f2)
by A52, FINSEQ_1:3;
then
len f2 in dom (Y_axis f2)
by A46, FINSEQ_1:def 3;
then A62:
(
(g2 /. 1) `2 <= (g1 /. i) `2 &
(g1 /. i) `2 <= (g2 /. (len g2)) `2 )
by A53, A54, A55, A58, A60, A61, GOBOARD1:def 4;
A63:
(Y_axis g1) . i = (g1 /. i) `2
by A44, GOBOARD1:def 4;
len g2 in Seg (len g2)
by A49, FINSEQ_1:3;
then
len g2 in dom (Y_axis g2)
by A48, FINSEQ_1:def 3;
hence
(
(Y_axis g2) . 1
<= (Y_axis g1) . i &
(Y_axis g1) . i <= (Y_axis g2) . (len g2) )
by A50, A62, A63, GOBOARD1:def 4;
:: thesis: verum
end;
then A64:
Y_axis g1 lies_between (Y_axis g2) . 1,(Y_axis g2) . (len g2)
by GOBOARD4:def 2;
for i being Element of 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
let i be
Element of
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) ) )
assume A65:
i in dom (Y_axis g2)
;
:: thesis: ( (Y_axis g2) . 1 <= (Y_axis g2) . i & (Y_axis g2) . i <= (Y_axis g2) . (len g2) )
A66:
(
len (Y_axis f2) = len f2 & ( for
j being
Element of
NAT st
j in dom (Y_axis f2) holds
(Y_axis f2) . j = (f2 /. j) `2 ) )
by GOBOARD1:def 4;
A67:
(
len (Y_axis g2) = len g2 & ( for
j being
Element of
NAT st
j in dom (Y_axis g2) holds
(Y_axis g2) . j = (g2 /. j) `2 ) )
by GOBOARD1:def 4;
A68:
1
<= len g2
by A3, XXREAL_0:2;
then
1
in Seg (len g2)
by FINSEQ_1:3;
then A69:
1
in dom (Y_axis g2)
by A67, FINSEQ_1:def 3;
A70:
g2 /. 1
= g2 . 1
by A68, FINSEQ_4:24;
A71:
1
<= len f2
by A1, XXREAL_0:2;
then A72:
g2 /. 1
= f2 /. 1
by A3, A70, FINSEQ_4:24;
g2 /. (len g2) = g2 . (len g2)
by A68, FINSEQ_4:24;
then A73:
g2 /. (len g2) = f2 /. (len f2)
by A3, A71, FINSEQ_4:24;
1
in Seg (len f2)
by A71, FINSEQ_1:3;
then A74:
1
in dom (Y_axis f2)
by A66, FINSEQ_1:def 3;
i in Seg (len g2)
by A65, A67, FINSEQ_1:def 3;
then A75:
i in dom g2
by FINSEQ_1:def 3;
then
g2 . i in rng g2
by FUNCT_1:def 5;
then consider y being
set such that A76:
(
y in dom f2 &
g2 . i = f2 . y )
by A3, FUNCT_1:def 5;
reconsider j =
y as
Element of
NAT by A76;
f2 . j = f2 /. j
by A76, PARTFUN1:def 8;
then A77:
(
j in dom f2 &
g2 /. i = f2 /. j )
by A75, A76, PARTFUN1:def 8;
j in Seg (len f2)
by A76, FINSEQ_1:def 3;
then A78:
j in dom (Y_axis f2)
by A66, FINSEQ_1:def 3;
then A79:
(
(Y_axis f2) . 1
<= (Y_axis f2) . j &
(Y_axis f2) . j <= (Y_axis f2) . (len f2) )
by A1, GOBOARD4:def 2;
A80:
(Y_axis f2) . j = (f2 /. j) `2
by A78, GOBOARD1:def 4;
len f2 in Seg (len f2)
by A71, FINSEQ_1:3;
then
len f2 in dom (Y_axis f2)
by A66, FINSEQ_1:def 3;
then A81:
(
(g2 /. 1) `2 <= (g2 /. i) `2 &
(g2 /. i) `2 <= (g2 /. (len g2)) `2 )
by A72, A73, A74, A77, A79, A80, GOBOARD1:def 4;
A82:
(Y_axis g2) . i = (g2 /. i) `2
by A65, GOBOARD1:def 4;
len g2 in Seg (len (Y_axis g2))
by A67, A68, FINSEQ_1:3;
then
len g2 in dom (Y_axis g2)
by FINSEQ_1:def 3;
hence
(
(Y_axis g2) . 1
<= (Y_axis g2) . i &
(Y_axis g2) . i <= (Y_axis g2) . (len g2) )
by A69, A81, A82, GOBOARD1:def 4;
:: thesis: verum
end;
then A83:
Y_axis g2 lies_between (Y_axis g2) . 1,(Y_axis g2) . (len g2)
by GOBOARD4:def 2;
A84:
for k being Element of NAT st k in dom g1 & k + 1 in dom g1 holds
g1 /. k <> g1 /. (k + 1)
for k being Element of NAT st k in dom g2 & k + 1 in dom g2 holds
g2 /. k <> g2 /. (k + 1)
then
L~ g1 meets L~ g2
by A2, A3, A22, A43, A64, A83, A84, GOBOARD4:4;
then
(L~ g1) /\ (L~ g2) <> {}
by XBOOLE_0:def 7;
then
(L~ f1) /\ (L~ f2) <> {}
by A2, A3, XBOOLE_1:3, XBOOLE_1:27;
hence
L~ f1 meets L~ f2
by XBOOLE_0:def 7; :: thesis: verum