let f1, f2 be FinSequence of (TOP-REAL 2); ( 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)
; 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)
for i being 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
Nat;
( 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)
;
( (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;
verum
end;
then A48:
Y_axis g1 lies_between (Y_axis g2) . 1,(Y_axis g2) . (len g2)
by GOBOARD4:def 2;
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
let i be
Nat;
( 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)
;
( (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;
verum
end;
then A68:
X_axis g2 lies_between (X_axis g1) . 1,(X_axis g1) . (len g1)
by GOBOARD4:def 2;
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
let i be
Nat;
( 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)
;
( (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;
verum
end;
then A88:
Y_axis g2 lies_between (Y_axis g2) . 1,(Y_axis g2) . (len g2)
by GOBOARD4:def 2;
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
let i be
Nat;
( 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)
;
( (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;
verum
end;
then A108:
X_axis g1 lies_between (X_axis g1) . 1,(X_axis g1) . (len g1)
by GOBOARD4:def 2;
for k being Nat st k in dom g1 & k + 1 in dom g1 holds
g1 /. k <> g1 /. (k + 1)
then
L~ g1 meets L~ g2
by A11, A12, A18, A19, A108, A68, A48, A88, A25, GOBOARD4:4;
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
; verum