:: GOBOARD2 semantic presentation
begin
theorem :: GOBOARD2:1
for f being FinSequence of (TOP-REAL 2) st ( for n, m being Element of NAT st m > n + 1 & n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f holds
LSeg (f,n) misses LSeg (f,m) ) holds
f is s.n.c.
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( ( for n, m being Element of NAT st m > n + 1 & n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f holds
LSeg (f,n) misses LSeg (f,m) ) implies f is s.n.c. )
assume A1: for n, m being Element of NAT st m > n + 1 & n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f holds
LSeg (f,n) misses LSeg (f,m) ; ::_thesis: f is s.n.c.
let n, m be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( m <= n + 1 or LSeg (f,n) misses LSeg (f,m) )
assume A2: m > n + 1 ; ::_thesis: LSeg (f,n) misses LSeg (f,m)
A3: ( n <= n + 1 & m <= m + 1 ) by NAT_1:11;
percases ( ( n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f ) or not n in dom f or not n + 1 in dom f or not m in dom f or not m + 1 in dom f ) ;
suppose ( n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f ) ; ::_thesis: LSeg (f,n) misses LSeg (f,m)
hence LSeg (f,n) misses LSeg (f,m) by A1, A2; ::_thesis: verum
end;
suppose ( not n in dom f or not n + 1 in dom f or not m in dom f or not m + 1 in dom f ) ; ::_thesis: LSeg (f,n) misses LSeg (f,m)
then ( not 1 <= n or not n <= len f or not 1 <= n + 1 or not n + 1 <= len f or not 1 <= m or not m <= len f or not 1 <= m + 1 or not m + 1 <= len f ) by FINSEQ_3:25;
then ( not 1 <= n or not n + 1 <= len f or not 1 <= m or not m + 1 <= len f ) by A3, XXREAL_0:2;
then ( LSeg (f,m) = {} or LSeg (f,n) = {} ) by TOPREAL1:def_3;
hence LSeg (f,n) misses LSeg (f,m) by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
theorem :: GOBOARD2:2
for f being FinSequence of (TOP-REAL 2)
for i being Element of NAT st f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f holds
i + 1 = len f
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f holds
i + 1 = len f
let i be Element of NAT ; ::_thesis: ( f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f implies i + 1 = len f )
assume that
A1: f is unfolded and
A2: f is s.n.c. and
A3: f is one-to-one and
A4: f /. (len f) in LSeg (f,i) and
A5: i in dom f and
A6: i + 1 in dom f and
A7: i + 1 <> len f ; ::_thesis: contradiction
A8: 1 <= i by A5, FINSEQ_3:25;
A9: i <= len f by A5, FINSEQ_3:25;
then reconsider l = (len f) - 1 as Element of NAT by A8, INT_1:5, XXREAL_0:2;
1 <= len f by A8, A9, XXREAL_0:2;
then A10: l + 1 in dom f by FINSEQ_3:25;
A11: i + 1 <= len f by A6, FINSEQ_3:25;
then i + 1 < len f by A7, XXREAL_0:1;
then A12: (i + 1) + 1 <= len f by NAT_1:13;
then A13: i + 1 <= (len f) - 1 by XREAL_1:19;
i <= l by A11, XREAL_1:19;
then A14: 1 <= l by A8, XXREAL_0:2;
then A15: f /. (l + 1) in LSeg (f,l) by TOPREAL1:21;
1 <= i + 1 by A6, FINSEQ_3:25;
then A16: f /. (i + 2) in LSeg (f,(i + 1)) by A12, TOPREAL1:21;
l <= len f by XREAL_1:43;
then A17: l in dom f by A14, FINSEQ_3:25;
l <> l + 1 ;
then A18: f /. l <> f /. (l + 1) by A3, A17, A10, PARTFUN2:10;
(i + 1) + 1 = i + (1 + 1) ;
then A19: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A1, A8, A12, TOPREAL1:def_6;
now__::_thesis:_contradiction
percases ( l = i + 1 or l <> i + 1 ) ;
supposeA20: l = i + 1 ; ::_thesis: contradiction
then f /. (len f) in (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by A4, A16, XBOOLE_0:def_4;
hence contradiction by A18, A19, A20, TARSKI:def_1; ::_thesis: verum
end;
suppose l <> i + 1 ; ::_thesis: contradiction
then i + 1 < l by A13, XXREAL_0:1;
then LSeg (f,i) misses LSeg (f,l) by A2, TOPREAL1:def_7;
then (LSeg (f,i)) /\ (LSeg (f,l)) = {} by XBOOLE_0:def_7;
hence contradiction by A4, A15, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem Th3: :: GOBOARD2:3
for f being FinSequence of (TOP-REAL 2)
for k being Element of NAT st k <> 0 & len f = k + 1 holds
L~ f = (L~ (f | k)) \/ (LSeg (f,k))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for k being Element of NAT st k <> 0 & len f = k + 1 holds
L~ f = (L~ (f | k)) \/ (LSeg (f,k))
let k be Element of NAT ; ::_thesis: ( k <> 0 & len f = k + 1 implies L~ f = (L~ (f | k)) \/ (LSeg (f,k)) )
assume that
A1: k <> 0 and
A2: len f = k + 1 ; ::_thesis: L~ f = (L~ (f | k)) \/ (LSeg (f,k))
A3: 0 + 1 <= k by A1, NAT_1:13;
set f1 = f | k;
set lf = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
set l1 = { (LSeg ((f | k),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } ;
k <= len f by A2, NAT_1:13;
then A4: len (f | k) = k by FINSEQ_1:59;
thus L~ f c= (L~ (f | k)) \/ (LSeg (f,k)) :: according to XBOOLE_0:def_10 ::_thesis: (L~ (f | k)) \/ (LSeg (f,k)) c= L~ f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in (L~ (f | k)) \/ (LSeg (f,k)) )
assume x in L~ f ; ::_thesis: x in (L~ (f | k)) \/ (LSeg (f,k))
then consider X being set such that
A5: x in X and
A6: X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def_4;
consider n being Element of NAT such that
A7: X = LSeg (f,n) and
A8: 1 <= n and
A9: n + 1 <= len f by A6;
now__::_thesis:_x_in_(L~_(f_|_k))_\/_(LSeg_(f,k))
percases ( n + 1 = len f or n + 1 <> len f ) ;
suppose n + 1 = len f ; ::_thesis: x in (L~ (f | k)) \/ (LSeg (f,k))
hence x in (L~ (f | k)) \/ (LSeg (f,k)) by A2, A5, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA10: n + 1 <> len f ; ::_thesis: x in (L~ (f | k)) \/ (LSeg (f,k))
A11: 1 <= n + 1 by A8, NAT_1:13;
n <= k by A2, A9, XREAL_1:6;
then A12: n in dom (f | k) by A4, A8, FINSEQ_3:25;
A13: n + 1 < len f by A9, A10, XXREAL_0:1;
then n + 1 <= k by A2, NAT_1:13;
then n + 1 in dom (f | k) by A4, A11, FINSEQ_3:25;
then A14: X = LSeg ((f | k),n) by A7, A12, TOPREAL3:17;
n + 1 <= k by A2, A13, NAT_1:13;
then X in { (LSeg ((f | k),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } by A4, A8, A14;
then x in union { (LSeg ((f | k),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } by A5, TARSKI:def_4;
hence x in (L~ (f | k)) \/ (LSeg (f,k)) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence x in (L~ (f | k)) \/ (LSeg (f,k)) ; ::_thesis: verum
end;
A15: k <= k + 1 by NAT_1:11;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (L~ (f | k)) \/ (LSeg (f,k)) or x in L~ f )
assume A16: x in (L~ (f | k)) \/ (LSeg (f,k)) ; ::_thesis: x in L~ f
now__::_thesis:_x_in_L~_f
percases ( x in L~ (f | k) or x in LSeg (f,k) ) by A16, XBOOLE_0:def_3;
suppose x in L~ (f | k) ; ::_thesis: x in L~ f
then consider X being set such that
A17: x in X and
A18: X in { (LSeg ((f | k),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } by TARSKI:def_4;
consider n being Element of NAT such that
A19: X = LSeg ((f | k),n) and
A20: 1 <= n and
A21: n + 1 <= len (f | k) by A18;
n <= n + 1 by NAT_1:11;
then n <= len (f | k) by A21, XXREAL_0:2;
then A22: n in dom (f | k) by A20, FINSEQ_3:25;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom (f | k) by A21, FINSEQ_3:25;
then A23: X = LSeg (f,n) by A19, A22, TOPREAL3:17;
n + 1 <= len f by A2, A15, A4, A21, XXREAL_0:2;
then X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A20, A23;
hence x in L~ f by A17, TARSKI:def_4; ::_thesis: verum
end;
supposeA24: x in LSeg (f,k) ; ::_thesis: x in L~ f
LSeg (f,k) in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A2, A3;
hence x in L~ f by A24, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in L~ f ; ::_thesis: verum
end;
theorem :: GOBOARD2:4
for f being FinSequence of (TOP-REAL 2)
for k being Element of NAT st 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. holds
(L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)}
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for k being Element of NAT st 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. holds
(L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)}
let k be Element of NAT ; ::_thesis: ( 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. implies (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)} )
assume that
A1: 1 < k and
A2: len f = k + 1 and
A3: f is unfolded and
A4: f is s.n.c. ; ::_thesis: (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)}
set f1 = f | k;
A5: len (f | k) = k by A2, FINSEQ_1:59, NAT_1:11;
reconsider k1 = k - 1 as Element of NAT by A1, INT_1:5;
set f2 = (f | k) | k1;
set l2 = { (LSeg (((f | k) | k1),m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len ((f | k) | k1) ) } ;
A6: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def_3;
A7: k in Seg k by A1, FINSEQ_1:1;
A8: dom ((f | k) | k1) = Seg (len ((f | k) | k1)) by FINSEQ_1:def_3;
A9: k1 < k by XREAL_1:44;
A10: k1 <= k by XREAL_1:44;
then A11: len ((f | k) | k1) = k1 by A5, FINSEQ_1:59;
A12: Seg k1 c= Seg k by A10, FINSEQ_1:5;
L~ ((f | k) | k1) misses LSeg (f,k)
proof
assume not L~ ((f | k) | k1) misses LSeg (f,k) ; ::_thesis: contradiction
then consider x being set such that
A13: x in L~ ((f | k) | k1) and
A14: x in LSeg (f,k) by XBOOLE_0:3;
consider X being set such that
A15: x in X and
A16: X in { (LSeg (((f | k) | k1),m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len ((f | k) | k1) ) } by A13, TARSKI:def_4;
consider n being Element of NAT such that
A17: X = LSeg (((f | k) | k1),n) and
A18: 1 <= n and
A19: n + 1 <= len ((f | k) | k1) by A16;
A20: ( n in dom ((f | k) | k1) & n + 1 in dom ((f | k) | k1) ) by A18, A19, SEQ_4:134;
then LSeg (((f | k) | k1),n) = LSeg ((f | k),n) by TOPREAL3:17;
then LSeg (((f | k) | k1),n) = LSeg (f,n) by A6, A12, A8, A5, A11, A20, TOPREAL3:17;
then A21: LSeg (f,n) meets LSeg (f,k) by A14, A15, A17, XBOOLE_0:3;
n + 1 < k by A9, A11, A19, XXREAL_0:2;
hence contradiction by A4, A21, TOPREAL1:def_7; ::_thesis: verum
end;
then A22: (L~ ((f | k) | k1)) /\ (LSeg (f,k)) = {} by XBOOLE_0:def_7;
A23: k + 1 = k1 + (1 + 1) ;
1 + 1 <= k by A1, NAT_1:13;
then A24: 1 <= k1 by XREAL_1:19;
then A25: k1 in Seg k by A10, FINSEQ_1:1;
k1 + 1 in Seg k by A1, FINSEQ_1:1;
then L~ (f | k) = (L~ ((f | k) | k1)) \/ (LSeg ((f | k),k1)) by A24, A5, Th3;
hence (L~ (f | k)) /\ (LSeg (f,k)) = {} \/ ((LSeg ((f | k),k1)) /\ (LSeg (f,k))) by A22, XBOOLE_1:23
.= (LSeg (f,k1)) /\ (LSeg (f,(k1 + 1))) by A6, A7, A25, A5, TOPREAL3:17
.= {(f /. k)} by A2, A3, A24, A23, TOPREAL1:def_6 ;
::_thesis: verum
end;
theorem :: GOBOARD2:5
for f1, f2 being FinSequence of (TOP-REAL 2)
for n, m being Element of NAT st len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n holds
LSeg ((f1 ^ f2),n) = LSeg (f2,m)
proof
let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: for n, m being Element of NAT st len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n holds
LSeg ((f1 ^ f2),n) = LSeg (f2,m)
let n, m be Element of NAT ; ::_thesis: ( len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n implies LSeg ((f1 ^ f2),n) = LSeg (f2,m) )
set f = f1 ^ f2;
assume that
A1: len f1 < n and
A2: n + 1 <= len (f1 ^ f2) and
A3: m + (len f1) = n ; ::_thesis: LSeg ((f1 ^ f2),n) = LSeg (f2,m)
A4: 1 <= m by A1, A3, NAT_1:19;
reconsider p = (f1 ^ f2) /. n, q = (f1 ^ f2) /. (n + 1) as Point of (TOP-REAL 2) ;
A5: n + 1 = (m + 1) + (len f1) by A3;
len (f1 ^ f2) = (len f1) + (len f2) by FINSEQ_1:22;
then A6: m + 1 <= len f2 by A2, A5, XREAL_1:6;
then A7: (f1 ^ f2) /. (n + 1) = f2 /. (m + 1) by A5, NAT_1:11, SEQ_4:136;
m <= m + 1 by NAT_1:11;
then m <= len f2 by A6, XXREAL_0:2;
then A8: (f1 ^ f2) /. n = f2 /. m by A3, A4, SEQ_4:136;
0 + 1 <= n by A1, NAT_1:13;
hence LSeg ((f1 ^ f2),n) = LSeg (p,q) by A2, TOPREAL1:def_3
.= LSeg (f2,m) by A4, A6, A8, A7, TOPREAL1:def_3 ;
::_thesis: verum
end;
theorem Th6: :: GOBOARD2:6
for f, g being FinSequence of (TOP-REAL 2) holds L~ f c= L~ (f ^ g)
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: L~ f c= L~ (f ^ g)
set f1 = f ^ g;
set lf = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
set l1 = { (LSeg ((f ^ g),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f ^ g) ) } ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in L~ (f ^ g) )
assume x in L~ f ; ::_thesis: x in L~ (f ^ g)
then consider X being set such that
A1: x in X and
A2: X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def_4;
consider n being Element of NAT such that
A3: X = LSeg (f,n) and
A4: 1 <= n and
A5: n + 1 <= len f by A2;
n <= n + 1 by NAT_1:11;
then n <= len f by A5, XXREAL_0:2;
then A6: n in dom f by A4, FINSEQ_3:25;
len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then len f <= len (f ^ g) by XREAL_1:31;
then A7: n + 1 <= len (f ^ g) by A5, XXREAL_0:2;
1 <= n + 1 by XREAL_1:31;
then n + 1 in dom f by A5, FINSEQ_3:25;
then X = LSeg ((f ^ g),n) by A3, A6, TOPREAL3:18;
then X in { (LSeg ((f ^ g),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f ^ g) ) } by A4, A7;
hence x in L~ (f ^ g) by A1, TARSKI:def_4; ::_thesis: verum
end;
theorem :: GOBOARD2:7
for f being FinSequence of (TOP-REAL 2)
for i being Element of NAT st f is s.n.c. holds
f | i is s.n.c.
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is s.n.c. holds
f | i is s.n.c.
let i be Element of NAT ; ::_thesis: ( f is s.n.c. implies f | i is s.n.c. )
assume A1: f is s.n.c. ; ::_thesis: f | i is s.n.c.
set f1 = f | i;
let n, m be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( m <= n + 1 or LSeg ((f | i),n) misses LSeg ((f | i),m) )
assume m > n + 1 ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)
then LSeg (f,n) misses LSeg (f,m) by A1, TOPREAL1:def_7;
then A2: (LSeg (f,n)) /\ (LSeg (f,m)) = {} by XBOOLE_0:def_7;
now__::_thesis:_LSeg_((f_|_i),n)_misses_LSeg_((f_|_i),m)
A3: m <= m + 1 by NAT_1:11;
A4: n <= n + 1 by NAT_1:11;
now__::_thesis:_LSeg_((f_|_i),n)_misses_LSeg_((f_|_i),m)
percases ( n in dom (f | i) or not n in dom (f | i) ) ;
supposeA5: n in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)
now__::_thesis:_LSeg_((f_|_i),n)_misses_LSeg_((f_|_i),m)
percases ( n + 1 in dom (f | i) or not n + 1 in dom (f | i) ) ;
suppose n + 1 in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)
then A6: LSeg (f,n) = LSeg ((f | i),n) by A5, TOPREAL3:17;
now__::_thesis:_LSeg_((f_|_i),n)_misses_LSeg_((f_|_i),m)
percases ( m in dom (f | i) or not m in dom (f | i) ) ;
supposeA7: m in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)
now__::_thesis:_(LSeg_((f_|_i),n))_/\_(LSeg_((f_|_i),m))_=_{}
percases ( m + 1 in dom (f | i) or not m + 1 in dom (f | i) ) ;
suppose m + 1 in dom (f | i) ; ::_thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {}
hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {} by A2, A6, A7, TOPREAL3:17; ::_thesis: verum
end;
suppose not m + 1 in dom (f | i) ; ::_thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {}
then ( not 1 <= m + 1 or not m + 1 <= len (f | i) ) by FINSEQ_3:25;
then LSeg ((f | i),m) = {} by NAT_1:11, TOPREAL1:def_3;
hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),m)) = {} ; ::_thesis: verum
end;
end;
end;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_0:def_7; ::_thesis: verum
end;
suppose not m in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)
then ( not 1 <= m or not m <= len (f | i) ) by FINSEQ_3:25;
then ( not 1 <= m or not m + 1 <= len (f | i) ) by A3, XXREAL_0:2;
then LSeg ((f | i),m) = {} by TOPREAL1:def_3;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; ::_thesis: verum
end;
suppose not n + 1 in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)
then ( not 1 <= n + 1 or not n + 1 <= len (f | i) ) by FINSEQ_3:25;
then LSeg ((f | i),n) = {} by NAT_1:11, TOPREAL1:def_3;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; ::_thesis: verum
end;
suppose not n in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),m)
then ( not 1 <= n or not n <= len (f | i) ) by FINSEQ_3:25;
then ( not 1 <= n or not n + 1 <= len (f | i) ) by A4, XXREAL_0:2;
then LSeg ((f | i),n) = {} by TOPREAL1:def_3;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; ::_thesis: verum
end;
hence LSeg ((f | i),n) misses LSeg ((f | i),m) ; ::_thesis: verum
end;
theorem :: GOBOARD2:8
for f1, f2 being FinSequence of (TOP-REAL 2) st f1 is special & f2 is special & ( (f1 /. (len f1)) `1 = (f2 /. 1) `1 or (f1 /. (len f1)) `2 = (f2 /. 1) `2 ) holds
f1 ^ f2 is special
proof
let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: ( f1 is special & f2 is special & ( (f1 /. (len f1)) `1 = (f2 /. 1) `1 or (f1 /. (len f1)) `2 = (f2 /. 1) `2 ) implies f1 ^ f2 is special )
assume that
A1: f1 is special and
A2: f2 is special and
A3: ( (f1 /. (len f1)) `1 = (f2 /. 1) `1 or (f1 /. (len f1)) `2 = (f2 /. 1) `2 ) ; ::_thesis: f1 ^ f2 is special
let n be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= n or not n + 1 <= len (f1 ^ f2) or ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )
set f = f1 ^ f2;
assume that
A4: 1 <= n and
A5: n + 1 <= len (f1 ^ f2) ; ::_thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )
reconsider n = n as Element of NAT by ORDINAL1:def_12;
set p = (f1 ^ f2) /. n;
set q = (f1 ^ f2) /. (n + 1);
A6: len (f1 ^ f2) = (len f1) + (len f2) by FINSEQ_1:22;
percases ( n + 1 <= len f1 or len f1 < n + 1 ) ;
supposeA7: n + 1 <= len f1 ; ::_thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )
then n + 1 in dom f1 by A4, SEQ_4:134;
then A8: f1 /. (n + 1) = (f1 ^ f2) /. (n + 1) by FINSEQ_4:68;
n in dom f1 by A4, A7, SEQ_4:134;
then f1 /. n = (f1 ^ f2) /. n by FINSEQ_4:68;
hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A1, A4, A7, A8, TOPREAL1:def_5; ::_thesis: verum
end;
suppose len f1 < n + 1 ; ::_thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )
then A9: len f1 <= n by NAT_1:13;
then reconsider n1 = n - (len f1) as Element of NAT by INT_1:5;
now__::_thesis:_(_((f1_^_f2)_/._n)_`1_=_((f1_^_f2)_/._(n_+_1))_`1_or_((f1_^_f2)_/._n)_`2_=_((f1_^_f2)_/._(n_+_1))_`2_)
percases ( n = len f1 or n <> len f1 ) ;
supposeA10: n = len f1 ; ::_thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )
then n in dom f1 by A4, FINSEQ_3:25;
then A11: (f1 ^ f2) /. n = f1 /. n by FINSEQ_4:68;
len f2 >= 1 by A5, A6, A10, XREAL_1:6;
hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A3, A10, A11, SEQ_4:136; ::_thesis: verum
end;
suppose n <> len f1 ; ::_thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )
then len f1 < n by A9, XXREAL_0:1;
then (len f1) + 1 <= n by NAT_1:13;
then A12: 1 <= n1 by XREAL_1:19;
A13: n + 1 = (n1 + 1) + (len f1) ;
then A14: n1 + 1 <= len f2 by A5, A6, XREAL_1:6;
then A15: f2 /. (n1 + 1) = (f1 ^ f2) /. (n + 1) by A13, NAT_1:11, SEQ_4:136;
n1 + 1 >= n1 by NAT_1:11;
then ( n = n1 + (len f1) & n1 <= len f2 ) by A14, XXREAL_0:2;
then f2 /. n1 = (f1 ^ f2) /. n by A12, SEQ_4:136;
hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A2, A12, A14, A15, TOPREAL1:def_5; ::_thesis: verum
end;
end;
end;
hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) ; ::_thesis: verum
end;
end;
end;
theorem Th9: :: GOBOARD2:9
for f being FinSequence of (TOP-REAL 2) st f <> {} holds
X_axis f <> {}
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f <> {} implies X_axis f <> {} )
A1: len (X_axis f) = len f by GOBOARD1:def_1;
assume ( f <> {} & X_axis f = {} ) ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
theorem Th10: :: GOBOARD2:10
for f being FinSequence of (TOP-REAL 2) st f <> {} holds
Y_axis f <> {}
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f <> {} implies Y_axis f <> {} )
A1: len (Y_axis f) = len f by GOBOARD1:def_2;
assume ( f <> {} & Y_axis f = {} ) ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
registration
let f be non empty FinSequence of (TOP-REAL 2);
cluster X_axis f -> non empty ;
coherence
not X_axis f is empty by Th9;
cluster Y_axis f -> non empty ;
coherence
not Y_axis f is empty by Th10;
end;
theorem Th11: :: GOBOARD2:11
for f being FinSequence of (TOP-REAL 2)
for G being Go-board st f is special holds
for n being Element of NAT st n in dom f & n + 1 in dom f holds
for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds
k = j
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st f is special holds
for n being Element of NAT st n in dom f & n + 1 in dom f holds
for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds
k = j
let G be Go-board; ::_thesis: ( f is special implies for n being Element of NAT st n in dom f & n + 1 in dom f holds
for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds
k = j )
assume A1: f is special ; ::_thesis: for n being Element of NAT st n in dom f & n + 1 in dom f holds
for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds
k = j
let n be Element of NAT ; ::_thesis: ( n in dom f & n + 1 in dom f implies for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds
k = j )
assume ( n in dom f & n + 1 in dom f ) ; ::_thesis: for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds
k = j
then A2: ( 1 <= n & n + 1 <= len f ) by FINSEQ_3:25;
let i, j, m, k be Element of NAT ; ::_thesis: ( [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m implies k = j )
assume that
A3: [i,j] in Indices G and
A4: [m,k] in Indices G and
A5: ( f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) ) ; ::_thesis: ( i = m or k = j )
reconsider cj = Col (G,j), lm = Line (G,m) as FinSequence of (TOP-REAL 2) ;
set xj = X_axis cj;
set yj = Y_axis cj;
set xm = X_axis lm;
set ym = Y_axis lm;
len cj = len G by MATRIX_1:def_8;
then A6: dom cj = dom G by FINSEQ_3:29;
assume that
A7: i <> m and
A8: k <> j ; ::_thesis: contradiction
A9: ( len (X_axis lm) = len lm & dom (X_axis lm) = Seg (len (X_axis lm)) ) by FINSEQ_1:def_3, GOBOARD1:def_1;
A10: len (X_axis cj) = len cj by GOBOARD1:def_1;
then A11: dom (X_axis cj) = dom cj by FINSEQ_3:29;
A12: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4;
then A13: i in dom G by A3, ZFMISC_1:87;
then cj /. i = cj . i by A6, PARTFUN1:def_6;
then A14: G * (i,j) = cj /. i by A13, MATRIX_1:def_8;
then A15: (X_axis cj) . i = (G * (i,j)) `1 by A13, A6, A11, GOBOARD1:def_1;
A16: m in dom G by A4, A12, ZFMISC_1:87;
then cj /. m = cj . m by A6, PARTFUN1:def_6;
then A17: G * (m,j) = cj /. m by A16, MATRIX_1:def_8;
then A18: (X_axis cj) . m = (G * (m,j)) `1 by A16, A6, A11, GOBOARD1:def_1;
A19: Y_axis lm is increasing by A16, GOBOARD1:def_6;
A20: X_axis lm is constant by A16, GOBOARD1:def_4;
A21: dom (Y_axis cj) = Seg (len (Y_axis cj)) by FINSEQ_1:def_3;
A22: ( dom (X_axis cj) = Seg (len (X_axis cj)) & len (Y_axis cj) = len cj ) by FINSEQ_1:def_3, GOBOARD1:def_2;
then A23: (Y_axis cj) . m = (G * (m,j)) `2 by A16, A10, A21, A6, A11, A17, GOBOARD1:def_2;
A24: j in Seg (width G) by A3, A12, ZFMISC_1:87;
then A25: X_axis cj is increasing by GOBOARD1:def_7;
A26: len lm = width G by MATRIX_1:def_7;
then A27: dom lm = Seg (width G) by FINSEQ_1:def_3;
then lm /. j = lm . j by A24, PARTFUN1:def_6;
then A28: G * (m,j) = lm /. j by A24, MATRIX_1:def_7;
then A29: (X_axis lm) . j = (G * (m,j)) `1 by A24, A26, A9, GOBOARD1:def_1;
A30: k in Seg (width G) by A4, A12, ZFMISC_1:87;
then lm /. k = lm . k by A27, PARTFUN1:def_6;
then A31: G * (m,k) = lm /. k by A30, MATRIX_1:def_7;
then A32: (X_axis lm) . k = (G * (m,k)) `1 by A30, A26, A9, GOBOARD1:def_1;
A33: Y_axis cj is constant by A24, GOBOARD1:def_5;
A34: ( len (Y_axis lm) = len lm & dom (Y_axis lm) = Seg (len (Y_axis lm)) ) by FINSEQ_1:def_3, GOBOARD1:def_2;
then A35: (Y_axis lm) . j = (G * (m,j)) `2 by A24, A26, A28, GOBOARD1:def_2;
A36: (Y_axis lm) . k = (G * (m,k)) `2 by A30, A26, A34, A31, GOBOARD1:def_2;
A37: (Y_axis cj) . i = (G * (i,j)) `2 by A13, A10, A22, A21, A6, A11, A14, GOBOARD1:def_2;
now__::_thesis:_contradiction
percases ( (G * (i,j)) `1 = (G * (m,k)) `1 or (G * (i,j)) `2 = (G * (m,k)) `2 ) by A1, A5, A2, TOPREAL1:def_5;
supposeA38: (G * (i,j)) `1 = (G * (m,k)) `1 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( i > m or i < m ) by A7, XXREAL_0:1;
suppose i > m ; ::_thesis: contradiction
then (G * (m,j)) `1 < (G * (i,j)) `1 by A13, A16, A6, A11, A25, A15, A18, SEQM_3:def_1;
hence contradiction by A24, A30, A26, A9, A20, A29, A32, A38, SEQM_3:def_10; ::_thesis: verum
end;
suppose i < m ; ::_thesis: contradiction
then (G * (m,j)) `1 > (G * (i,j)) `1 by A13, A16, A6, A11, A25, A15, A18, SEQM_3:def_1;
hence contradiction by A24, A30, A26, A9, A20, A29, A32, A38, SEQM_3:def_10; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
supposeA39: (G * (i,j)) `2 = (G * (m,k)) `2 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( k > j or k < j ) by A8, XXREAL_0:1;
suppose k > j ; ::_thesis: contradiction
then (G * (m,j)) `2 < (G * (m,k)) `2 by A24, A30, A26, A34, A19, A35, A36, SEQM_3:def_1;
hence contradiction by A13, A16, A10, A22, A21, A6, A11, A33, A37, A23, A39, SEQM_3:def_10; ::_thesis: verum
end;
suppose k < j ; ::_thesis: contradiction
then (G * (m,j)) `2 > (G * (m,k)) `2 by A24, A30, A26, A34, A19, A35, A36, SEQM_3:def_1;
hence contradiction by A13, A16, A10, A22, A21, A6, A11, A33, A37, A23, A39, SEQM_3:def_10; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem :: GOBOARD2:12
for f being FinSequence of (TOP-REAL 2)
for G being Go-board st ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ) holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for G being Go-board st ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ) holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
let G be Go-board; ::_thesis: ( ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) )
defpred S1[ Element of NAT ] means for f being FinSequence of (TOP-REAL 2) st len f = $1 & ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ) holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g );
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f = k + 1 & ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) )
assume that
A3: len f = k + 1 and
A4: for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) and
A5: f is special and
A6: for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
A7: dom f = Seg (len f) by FINSEQ_1:def_3;
now__::_thesis:_ex_g_being_FinSequence_of_(TOP-REAL_2)_st_
(_g_is_sequence_on_G_&_L~_f_=_L~_g_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_)
percases ( k = 0 or k <> 0 ) ;
supposeA8: k = 0 ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
take g = f; ::_thesis: ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
A9: dom f = {1} by A3, A8, FINSEQ_1:2, FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g_&_n_+_1_in_dom_g_holds_
for_i1,_i2,_j1,_j2_being_Element_of_NAT_st_[i1,i2]_in_Indices_G_&_[j1,j2]_in_Indices_G_&_g_/._n_=_G_*_(i1,i2)_&_g_/._(n_+_1)_=_G_*_(j1,j2)_holds_
(abs_(i1_-_j1))_+_(abs_(i2_-_j2))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom g & n + 1 in dom g implies for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 )
assume that
A10: n in dom g and
A11: n + 1 in dom g ; ::_thesis: for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1
n = 1 by A9, A10, TARSKI:def_1;
hence for i1, i2, j1, j2 being Element of NAT st [i1,i2] in Indices G & [j1,j2] in Indices G & g /. n = G * (i1,i2) & g /. (n + 1) = G * (j1,j2) holds
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A9, A11, TARSKI:def_1; ::_thesis: verum
end;
hence ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) by A4, GOBOARD1:def_9; ::_thesis: verum
end;
supposeA12: k <> 0 ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
then A13: 0 + 1 <= k by NAT_1:13;
then A14: k in Seg k by FINSEQ_1:1;
A15: 1 in Seg k by A13, FINSEQ_1:1;
A16: k <= k + 1 by NAT_1:11;
then A17: k in dom f by A3, A7, A13, FINSEQ_1:1;
then consider i1, i2 being Element of NAT such that
A18: [i1,i2] in Indices G and
A19: f /. k = G * (i1,i2) by A4;
reconsider l1 = Line (G,i1), c1 = Col (G,i2) as FinSequence of (TOP-REAL 2) ;
set x1 = X_axis l1;
set y1 = Y_axis l1;
set x2 = X_axis c1;
set y2 = Y_axis c1;
A20: ( dom (Y_axis l1) = Seg (len (Y_axis l1)) & len (Y_axis l1) = len l1 ) by FINSEQ_1:def_3, GOBOARD1:def_2;
len (Y_axis c1) = len c1 by GOBOARD1:def_2;
then A21: dom (Y_axis c1) = dom c1 by FINSEQ_3:29;
len (X_axis c1) = len c1 by GOBOARD1:def_1;
then A22: dom (X_axis c1) = dom c1 by FINSEQ_3:29;
set f1 = f | k;
A23: len (f | k) = k by A3, FINSEQ_1:59, NAT_1:11;
A24: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def_3;
A25: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(f_|_k)_holds_
ex_i,_j_being_Element_of_NAT_st_
(_[i,j]_in_Indices_G_&_(f_|_k)_/._n_=_G_*_(i,j)_)
let n be Element of NAT ; ::_thesis: ( n in dom (f | k) implies ex i, j being Element of NAT st
( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) )
assume A26: n in dom (f | k) ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices G & (f | k) /. n = G * (i,j) )
then n in dom f by A17, A23, A24, FINSEQ_4:71;
then consider i, j being Element of NAT such that
A27: ( [i,j] in Indices G & f /. n = G * (i,j) ) by A4;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices G & (f | k) /. n = G * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices G & (f | k) /. n = G * (i,j) )
thus ( [i,j] in Indices G & (f | k) /. n = G * (i,j) ) by A17, A23, A24, A26, A27, FINSEQ_4:71; ::_thesis: verum
end;
A28: f | k is special
proof
let n be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= n or not n + 1 <= len (f | k) or ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 )
assume that
A29: 1 <= n and
A30: n + 1 <= len (f | k) ; ::_thesis: ( ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 )
n <= n + 1 by NAT_1:11;
then n <= len (f | k) by A30, XXREAL_0:2;
then n in dom (f | k) by A29, FINSEQ_3:25;
then A31: (f | k) /. n = f /. n by A17, A23, A24, FINSEQ_4:71;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom (f | k) by A30, FINSEQ_3:25;
then A32: (f | k) /. (n + 1) = f /. (n + 1) by A17, A23, A24, FINSEQ_4:71;
n + 1 <= len f by A3, A16, A23, A30, XXREAL_0:2;
hence ( ((f | k) /. n) `1 = ((f | k) /. (n + 1)) `1 or ((f | k) /. n) `2 = ((f | k) /. (n + 1)) `2 ) by A5, A29, A31, A32, TOPREAL1:def_5; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(f_|_k)_&_n_+_1_in_dom_(f_|_k)_holds_
(f_|_k)_/._n_<>_(f_|_k)_/._(n_+_1)
let n be Element of NAT ; ::_thesis: ( n in dom (f | k) & n + 1 in dom (f | k) implies (f | k) /. n <> (f | k) /. (n + 1) )
assume A33: ( n in dom (f | k) & n + 1 in dom (f | k) ) ; ::_thesis: (f | k) /. n <> (f | k) /. (n + 1)
then A34: ( (f | k) /. n = f /. n & (f | k) /. (n + 1) = f /. (n + 1) ) by A17, A23, A24, FINSEQ_4:71;
( n in dom f & n + 1 in dom f ) by A17, A23, A24, A33, FINSEQ_4:71;
hence (f | k) /. n <> (f | k) /. (n + 1) by A6, A34; ::_thesis: verum
end;
then consider g1 being FinSequence of (TOP-REAL 2) such that
A35: g1 is_sequence_on G and
A36: L~ g1 = L~ (f | k) and
A37: g1 /. 1 = (f | k) /. 1 and
A38: g1 /. (len g1) = (f | k) /. (len (f | k)) and
A39: len (f | k) <= len g1 by A2, A23, A25, A28;
A40: for n being Element of NAT st n in dom g1 holds
ex m, k being Element of NAT st
( [m,k] in Indices G & g1 /. n = G * (m,k) ) by A35, GOBOARD1:def_9;
A41: for n being Element of NAT st n in dom g1 & n + 1 in dom g1 holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g1 /. n = G * (m,k) & g1 /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A35, GOBOARD1:def_9;
A42: ( dom (X_axis l1) = Seg (len (X_axis l1)) & len (X_axis l1) = len l1 ) by FINSEQ_1:def_3, GOBOARD1:def_1;
len c1 = len G by MATRIX_1:def_8;
then A43: dom c1 = dom G by FINSEQ_3:29;
1 <= len f by A3, NAT_1:11;
then A44: k + 1 in dom f by A3, FINSEQ_3:25;
then consider j1, j2 being Element of NAT such that
A45: [j1,j2] in Indices G and
A46: f /. (k + 1) = G * (j1,j2) by A4;
A47: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def_4;
then A48: j1 in dom G by A45, ZFMISC_1:87;
A49: i1 in dom G by A18, A47, ZFMISC_1:87;
then A50: X_axis l1 is constant by GOBOARD1:def_4;
A51: i2 in Seg (width G) by A18, A47, ZFMISC_1:87;
then A52: X_axis c1 is increasing by GOBOARD1:def_7;
A53: Y_axis c1 is constant by A51, GOBOARD1:def_5;
A54: Y_axis l1 is increasing by A49, GOBOARD1:def_6;
A55: len l1 = width G by MATRIX_1:def_7;
A56: j2 in Seg (width G) by A45, A47, ZFMISC_1:87;
A57: dom g1 = Seg (len g1) by FINSEQ_1:def_3;
now__::_thesis:_ex_g_being_FinSequence_of_(TOP-REAL_2)_st_
(_g_is_sequence_on_G_&_L~_f_=_L~_g_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_)
percases ( i1 = j1 or i2 = j2 ) by A5, A17, A18, A19, A44, A45, A46, Th11;
supposeA58: i1 = j1 ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
set ppi = G * (i1,i2);
set pj = G * (i1,j2);
now__::_thesis:_(_(_i2_>_j2_&_ex_g_being_FinSequence_of_the_carrier_of_(TOP-REAL_2)_st_
(_g_is_sequence_on_G_&_L~_g_=_L~_f_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_)_)_or_(_i2_=_j2_&_contradiction_)_or_(_i2_<_j2_&_ex_g_being_FinSequence_of_the_carrier_of_(TOP-REAL_2)_st_
(_g_is_sequence_on_G_&_L~_g_=_L~_f_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_)_)_)
percases ( i2 > j2 or i2 = j2 or i2 < j2 ) by XXREAL_0:1;
caseA59: i2 > j2 ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st
( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
j2 in dom l1 by A56, A55, FINSEQ_1:def_3;
then l1 /. j2 = l1 . j2 by PARTFUN1:def_6;
then A60: l1 /. j2 = G * (i1,j2) by A56, MATRIX_1:def_7;
then A61: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, GOBOARD1:def_2;
i2 in dom l1 by A51, A55, FINSEQ_1:def_3;
then l1 /. i2 = l1 . i2 by PARTFUN1:def_6;
then A62: l1 /. i2 = G * (i1,i2) by A51, MATRIX_1:def_7;
then A63: (Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, GOBOARD1:def_2;
then A64: (G * (i1,j2)) `2 < (G * (i1,i2)) `2 by A51, A56, A54, A20, A55, A59, A61, SEQM_3:def_1;
A65: (X_axis l1) . j2 = (G * (i1,j2)) `1 by A56, A42, A55, A60, GOBOARD1:def_1;
(X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A62, GOBOARD1:def_1;
then A66: (G * (i1,i2)) `1 = (G * (i1,j2)) `1 by A51, A56, A50, A42, A55, A65, SEQM_3:def_10;
reconsider l = i2 - j2 as Element of NAT by A59, INT_1:5;
defpred S2[ Nat, set ] means for m being Element of NAT st m = i2 - $1 holds
$2 = G * (i1,m);
set lk = { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= w `2 & w `2 <= (G * (i1,i2)) `2 ) } ;
A67: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;
A68: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_Seg_l_holds_
(_i2_-_n_is_Element_of_NAT_&_[i1,(i2_-_n)]_in_Indices_G_&_i2_-_n_in_Seg_(width_G)_)
let n be Element of NAT ; ::_thesis: ( n in Seg l implies ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) ) )
assume n in Seg l ; ::_thesis: ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) )
then A69: n <= l by FINSEQ_1:1;
l <= i2 by XREAL_1:43;
then reconsider w = i2 - n as Element of NAT by A69, INT_1:5, XXREAL_0:2;
( i2 - n <= i2 & i2 <= width G ) by A51, FINSEQ_1:1, XREAL_1:43;
then A70: w <= width G by XXREAL_0:2;
A71: 1 <= j2 by A56, FINSEQ_1:1;
i2 - l <= i2 - n by A69, XREAL_1:13;
then 1 <= w by A71, XXREAL_0:2;
then w in Seg (width G) by A70, FINSEQ_1:1;
hence ( i2 - n is Element of NAT & [i1,(i2 - n)] in Indices G & i2 - n in Seg (width G) ) by A47, A49, ZFMISC_1:87; ::_thesis: verum
end;
A72: now__::_thesis:_for_n_being_Nat_st_n_in_Seg_l_holds_
ex_p_being_Element_of_the_carrier_of_(TOP-REAL_2)_st_S2[n,p]
let n be Nat; ::_thesis: ( n in Seg l implies ex p being Element of the carrier of (TOP-REAL 2) st S2[n,p] )
assume n in Seg l ; ::_thesis: ex p being Element of the carrier of (TOP-REAL 2) st S2[n,p]
then reconsider m = i2 - n as Element of NAT by A68;
take p = G * (i1,m); ::_thesis: S2[n,p]
thus S2[n,p] ; ::_thesis: verum
end;
consider g2 being FinSequence of (TOP-REAL 2) such that
A73: ( len g2 = l & ( for n being Nat st n in Seg l holds
S2[n,g2 /. n] ) ) from FINSEQ_4:sch_1(A72);
take g = g1 ^ g2; ::_thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
A74: dom g2 = Seg l by A73, FINSEQ_1:def_3;
A75: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_&_n_+_1_in_dom_g2_holds_
for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g2_/._n_=_G_*_(l1,l2)_&_g2_/._(n_+_1)_=_G_*_(l3,l4)_holds_
(abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds
(abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A76: n in dom g2 and
A77: n + 1 in dom g2 ; ::_thesis: for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds
(abs (l1 - l3)) + (abs (l2 - l4)) = 1
reconsider m1 = i2 - n, m2 = i2 - (n + 1) as Element of NAT by A68, A74, A76, A77;
let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A78: [l1,l2] in Indices G and
A79: [l3,l4] in Indices G and
A80: g2 /. n = G * (l1,l2) and
A81: g2 /. (n + 1) = G * (l3,l4) ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1
( [i1,(i2 - (n + 1))] in Indices G & g2 /. (n + 1) = G * (i1,m2) ) by A68, A73, A74, A77;
then A82: ( l3 = i1 & l4 = m2 ) by A79, A81, GOBOARD1:5;
( [i1,(i2 - n)] in Indices G & g2 /. n = G * (i1,m1) ) by A68, A73, A74, A76;
then ( l1 = i1 & l2 = m1 ) by A78, A80, GOBOARD1:5;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs ((i2 - n) - (i2 - (n + 1)))) by A82, ABSVALUE:2
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_holds_
ex_k,_m_being_Element_of_NAT_st_
(_[k,m]_in_Indices_G_&_g2_/._n_=_G_*_(k,m)_)
let n be Element of NAT ; ::_thesis: ( n in dom g2 implies ex k, m being Element of NAT st
( [k,m] in Indices G & g2 /. n = G * (k,m) ) )
assume A83: n in dom g2 ; ::_thesis: ex k, m being Element of NAT st
( [k,m] in Indices G & g2 /. n = G * (k,m) )
then reconsider m = i2 - n as Element of NAT by A68, A74;
take k = i1; ::_thesis: ex m being Element of NAT st
( [k,m] in Indices G & g2 /. n = G * (k,m) )
take m = m; ::_thesis: ( [k,m] in Indices G & g2 /. n = G * (k,m) )
thus ( [k,m] in Indices G & g2 /. n = G * (k,m) ) by A68, A73, A74, A83; ::_thesis: verum
end;
then A84: for n being Element of NAT st n in dom g holds
ex i, j being Element of NAT st
( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;
now__::_thesis:_for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g1_/._(len_g1)_=_G_*_(l1,l2)_&_g2_/._1_=_G_*_(l3,l4)_&_len_g1_in_dom_g1_&_1_in_dom_g2_holds_
(abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1
let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A85: [l1,l2] in Indices G and
A86: [l3,l4] in Indices G and
A87: g1 /. (len g1) = G * (l1,l2) and
A88: g2 /. 1 = G * (l3,l4) and
len g1 in dom g1 and
A89: 1 in dom g2 ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1
reconsider m1 = i2 - 1 as Element of NAT by A68, A74, A89;
( [i1,(i2 - 1)] in Indices G & g2 /. 1 = G * (i1,m1) ) by A68, A73, A74, A89;
then A90: ( l3 = i1 & l4 = m1 ) by A86, A88, GOBOARD1:5;
(f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71;
then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A85, A87, GOBOARD1:5;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs (i2 - (i2 - 1))) by A90, ABSVALUE:2
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
then for n being Element of NAT st n in dom g & n + 1 in dom g holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A41, A75, GOBOARD1:24;
hence g is_sequence_on G by A84, GOBOARD1:def_9; ::_thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
reconsider m1 = i2 - l as Element of NAT ;
A91: G * (i1,j2) = |[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| by EUCLID:53;
A92: LSeg (f,k) = LSeg ((G * (i1,j2)),(G * (i1,i2))) by A3, A13, A19, A46, A58, TOPREAL1:def_3
.= { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= w `2 & w `2 <= (G * (i1,i2)) `2 ) } by A64, A66, A67, A91, TOPREAL3:9 ;
thus L~ g = L~ f ::_thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
proof
set lg = { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ;
set lf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
A93: len g = (len g1) + (len g2) by FINSEQ_1:22;
A94: now__::_thesis:_for_j_being_Element_of_NAT_st_len_g1_<=_j_&_j_<=_len_g_holds_
for_p_being_Point_of_(TOP-REAL_2)_st_p_=_g_/._j_holds_
(_p_`1_=_(G_*_(i1,i2))_`1_&_(G_*_(i1,j2))_`2_<=_p_`2_&_p_`2_<=_(G_*_(i1,i2))_`2_&_p_in_rng_l1_)
let j be Element of NAT ; ::_thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds
( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) )
assume that
A95: len g1 <= j and
A96: j <= len g ; ::_thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds
( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )
reconsider w = j - (len g1) as Element of NAT by A95, INT_1:5;
let p be Point of (TOP-REAL 2); ::_thesis: ( p = g /. j implies ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) )
assume A97: p = g /. j ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )
A98: dom l1 = Seg (len l1) by FINSEQ_1:def_3;
now__::_thesis:_(_p_`1_=_(G_*_(i1,i2))_`1_&_(G_*_(i1,j2))_`2_<=_p_`2_&_p_`2_<=_(G_*_(i1,i2))_`2_&_p_in_rng_l1_)
percases ( j = len g1 or j <> len g1 ) ;
supposeA99: j = len g1 ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then A100: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68
.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;
hence p `1 = (G * (i1,i2)) `1 by A97, A99; ::_thesis: ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )
thus ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 ) by A51, A56, A54, A20, A55, A59, A63, A61, A97, A99, A100, SEQM_3:def_1; ::_thesis: p in rng l1
thus p in rng l1 by A51, A55, A62, A97, A98, A99, A100, PARTFUN2:2; ::_thesis: verum
end;
supposeA101: j <> len g1 ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )
A102: w + (len g1) = j ;
then A103: w <= len g2 by A93, A96, XREAL_1:6;
A104: j - (len g1) <> 0 by A101;
then A105: w >= 1 by NAT_1:14;
then A106: w in dom g2 by A103, FINSEQ_3:25;
then reconsider u = i2 - w as Element of NAT by A68, A74;
A107: g /. j = g2 /. w by A105, A102, A103, SEQ_4:136;
A108: (X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A62, GOBOARD1:def_1;
A109: u < i2 by A104, XREAL_1:44;
A110: g2 /. w = G * (i1,u) by A73, A74, A106;
A111: i2 - w in Seg (width G) by A68, A74, A106;
then u in dom l1 by A55, FINSEQ_1:def_3;
then l1 /. u = l1 . u by PARTFUN1:def_6;
then A112: l1 /. u = G * (i1,u) by A111, MATRIX_1:def_7;
then A113: (Y_axis l1) . u = (G * (i1,u)) `2 by A20, A55, A111, GOBOARD1:def_2;
(X_axis l1) . u = (G * (i1,u)) `1 by A42, A55, A111, A112, GOBOARD1:def_1;
hence p `1 = (G * (i1,i2)) `1 by A51, A50, A42, A55, A97, A107, A111, A110, A108, SEQM_3:def_10; ::_thesis: ( (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 )
A114: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, A60, GOBOARD1:def_2;
now__::_thesis:_(G_*_(i1,j2))_`2_<=_p_`2
percases ( u = j2 or u <> j2 ) ;
suppose u = j2 ; ::_thesis: (G * (i1,j2)) `2 <= p `2
hence (G * (i1,j2)) `2 <= p `2 by A97, A105, A102, A103, A110, SEQ_4:136; ::_thesis: verum
end;
supposeA115: u <> j2 ; ::_thesis: (G * (i1,j2)) `2 <= p `2
i2 - (len g2) <= u by A103, XREAL_1:13;
then j2 < u by A73, A115, XXREAL_0:1;
hence (G * (i1,j2)) `2 <= p `2 by A56, A54, A20, A55, A97, A107, A111, A110, A113, A114, SEQM_3:def_1; ::_thesis: verum
end;
end;
end;
hence (G * (i1,j2)) `2 <= p `2 ; ::_thesis: ( p `2 <= (G * (i1,i2)) `2 & p in rng l1 )
(Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, A62, GOBOARD1:def_2;
hence p `2 <= (G * (i1,i2)) `2 by A51, A54, A20, A55, A97, A107, A111, A110, A113, A109, SEQM_3:def_1; ::_thesis: p in rng l1
thus p in rng l1 by A55, A97, A98, A107, A111, A110, A112, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
hence ( p `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= p `2 & p `2 <= (G * (i1,i2)) `2 & p in rng l1 ) ; ::_thesis: verum
end;
thus L~ g c= L~ f :: according to XBOOLE_0:def_10 ::_thesis: L~ f c= L~ g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ g or x in L~ f )
assume x in L~ g ; ::_thesis: x in L~ f
then consider X being set such that
A116: x in X and
A117: X in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def_4;
consider i being Element of NAT such that
A118: X = LSeg (g,i) and
A119: 1 <= i and
A120: i + 1 <= len g by A117;
now__::_thesis:_x_in_L~_f
percases ( i + 1 <= len g1 or i + 1 > len g1 ) ;
supposeA121: i + 1 <= len g1 ; ::_thesis: x in L~ f
i <= i + 1 by NAT_1:11;
then i <= len g1 by A121, XXREAL_0:2;
then A122: i in dom g1 by A119, FINSEQ_3:25;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom g1 by A121, FINSEQ_3:25;
then X = LSeg (g1,i) by A118, A122, TOPREAL3:18;
then X in { (LSeg (g1,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A119, A121;
then A123: x in L~ (f | k) by A36, A116, TARSKI:def_4;
L~ (f | k) c= L~ f by TOPREAL3:20;
hence x in L~ f by A123; ::_thesis: verum
end;
supposeA124: i + 1 > len g1 ; ::_thesis: x in L~ f
reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;
A125: i <= len g by A120, NAT_1:13;
A126: len g1 <= i by A124, NAT_1:13;
then A127: q1 `1 = (G * (i1,i2)) `1 by A94, A125;
A128: q1 `2 <= (G * (i1,i2)) `2 by A94, A126, A125;
A129: (G * (i1,j2)) `2 <= q1 `2 by A94, A126, A125;
q2 `1 = (G * (i1,i2)) `1 by A94, A120, A124;
then A130: q2 = |[(q1 `1),(q2 `2)]| by A127, EUCLID:53;
A131: q2 `2 <= (G * (i1,i2)) `2 by A94, A120, A124;
A132: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A119, A120, EUCLID:53, TOPREAL1:def_3;
A133: (G * (i1,j2)) `2 <= q2 `2 by A94, A120, A124;
now__::_thesis:_x_in_L~_f
percases ( q1 `2 > q2 `2 or q1 `2 = q2 `2 or q1 `2 < q2 `2 ) by XXREAL_0:1;
suppose q1 `2 > q2 `2 ; ::_thesis: x in L~ f
then LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q1 `1 & q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) } by A130, A132, TOPREAL3:9;
then consider p2 being Point of (TOP-REAL 2) such that
A134: ( p2 = x & p2 `1 = q1 `1 ) and
A135: ( q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by A116, A118;
( (G * (i1,j2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,i2)) `2 ) by A128, A133, A135, XXREAL_0:2;
then A136: x in LSeg (f,k) by A92, A127, A134;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A136, TARSKI:def_4; ::_thesis: verum
end;
suppose q1 `2 = q2 `2 ; ::_thesis: x in L~ f
then LSeg (g,i) = {q1} by A130, A132, RLTOPSP1:70;
then x = q1 by A116, A118, TARSKI:def_1;
then A137: x in LSeg (f,k) by A92, A127, A129, A128;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A137, TARSKI:def_4; ::_thesis: verum
end;
suppose q1 `2 < q2 `2 ; ::_thesis: x in L~ f
then LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = q1 `1 & q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) } by A130, A132, TOPREAL3:9;
then consider p2 being Point of (TOP-REAL 2) such that
A138: ( p2 = x & p2 `1 = q1 `1 ) and
A139: ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A116, A118;
( (G * (i1,j2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,i2)) `2 ) by A129, A131, A139, XXREAL_0:2;
then A140: x in LSeg (f,k) by A92, A127, A138;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A140, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in L~ f ; ::_thesis: verum
end;
end;
end;
hence x in L~ f ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in L~ g )
assume x in L~ f ; ::_thesis: x in L~ g
then A141: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3;
now__::_thesis:_x_in_L~_g
percases ( x in L~ (f | k) or x in LSeg (f,k) ) by A141, XBOOLE_0:def_3;
supposeA142: x in L~ (f | k) ; ::_thesis: x in L~ g
L~ g1 c= L~ g by Th6;
hence x in L~ g by A36, A142; ::_thesis: verum
end;
suppose x in LSeg (f,k) ; ::_thesis: x in L~ g
then consider p1 being Point of (TOP-REAL 2) such that
A143: p1 = x and
A144: p1 `1 = (G * (i1,i2)) `1 and
A145: (G * (i1,j2)) `2 <= p1 `2 and
A146: p1 `2 <= (G * (i1,i2)) `2 by A92;
defpred S3[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds
q `2 >= p1 `2 ) );
A147: now__::_thesis:_ex_n_being_Nat_st_S3[n]
reconsider n = len g1 as Nat ;
take n = n; ::_thesis: S3[n]
thus S3[n] ::_thesis: verum
proof
thus ( len g1 <= n & n <= len g ) by A93, XREAL_1:31; ::_thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds
q `2 >= p1 `2
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then A148: len g1 in dom g1 by FINSEQ_3:25;
let q be Point of (TOP-REAL 2); ::_thesis: ( q = g /. n implies q `2 >= p1 `2 )
assume q = g /. n ; ::_thesis: q `2 >= p1 `2
then q = (f | k) /. (len (f | k)) by A38, A148, FINSEQ_4:68
.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;
hence q `2 >= p1 `2 by A146; ::_thesis: verum
end;
end;
A149: for n being Nat st S3[n] holds
n <= len g ;
consider ma being Nat such that
A150: ( S3[ma] & ( for n being Nat st S3[n] holds
n <= ma ) ) from NAT_1:sch_6(A149, A147);
reconsider ma = ma as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_x_in_L~_g
percases ( ma = len g or ma <> len g ) ;
supposeA151: ma = len g ; ::_thesis: x in L~ g
j2 + 1 <= i2 by A59, NAT_1:13;
then A152: 1 <= l by XREAL_1:19;
then 0 + 1 <= ma by A73, A93, A151, XREAL_1:7;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;
A153: m1 + 1 = ma ;
(len g1) + 1 <= ma by A73, A93, A151, A152, XREAL_1:7;
then A154: m1 >= len g1 by A153, XREAL_1:6;
reconsider q = g /. m1 as Point of (TOP-REAL 2) ;
set lq = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= e `2 & e `2 <= q `2 ) } ;
A155: i2 - l = j2 ;
A156: l in dom g2 by A74, A152, FINSEQ_1:1;
then A157: g /. ma = g2 /. l by A73, A93, A151, FINSEQ_4:69
.= G * (i1,j2) by A73, A74, A156, A155 ;
then p1 `2 <= (G * (i1,j2)) `2 by A150;
then A158: p1 `2 = (G * (i1,j2)) `2 by A145, XXREAL_0:1;
A159: m1 <= len g by A151, A153, NAT_1:11;
then A160: q `1 = (G * (i1,i2)) `1 by A94, A154;
A161: (G * (i1,j2)) `2 <= q `2 by A94, A154, A159;
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then A162: 1 <= m1 by A154, XXREAL_0:2;
then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (i1,j2)),q) ) by A151, A157, A153, EUCLID:53, TOPREAL1:def_3;
then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= e `2 & e `2 <= q `2 ) } by A66, A91, A160, A161, TOPREAL3:9;
then A163: p1 in LSeg (g,m1) by A144, A158, A161;
LSeg (g,m1) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A151, A153, A162;
hence x in L~ g by A143, A163, TARSKI:def_4; ::_thesis: verum
end;
suppose ma <> len g ; ::_thesis: x in L~ g
then ma < len g by A150, XXREAL_0:1;
then A164: ma + 1 <= len g by NAT_1:13;
reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;
set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa1 `2 <= p2 `2 & p2 `2 <= qa `2 ) } ;
A165: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53;
A166: p1 `2 <= qa `2 by A150;
A167: len g1 <= ma + 1 by A150, NAT_1:13;
then A168: qa1 `1 = (G * (i1,i2)) `1 by A94, A164;
A169: now__::_thesis:_not_p1_`2_<=_qa1_`2
assume p1 `2 <= qa1 `2 ; ::_thesis: contradiction
then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds
p1 `2 <= q `2 ;
then ma + 1 <= ma by A150, A164, A167;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
A170: ( qa `1 = (G * (i1,i2)) `1 & qa = |[(qa `1),(qa `2)]| ) by A94, A150, EUCLID:53;
A171: 1 <= ma by A13, A23, A39, A150, NAT_1:13;
then LSeg (g,ma) = LSeg (qa1,qa) by A164, TOPREAL1:def_3
.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa1 `2 <= p2 `2 & p2 `2 <= qa `2 ) } by A166, A169, A168, A170, A165, TOPREAL3:9, XXREAL_0:2 ;
then A172: x in LSeg (g,ma) by A143, A144, A166, A169;
LSeg (g,ma) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A171, A164;
hence x in L~ g by A172, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in L~ g ; ::_thesis: verum
end;
end;
end;
hence x in L~ g ; ::_thesis: verum
end;
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:25;
hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68
.= f /. 1 by A17, A15, FINSEQ_4:71 ;
::_thesis: ( g /. (len g) = f /. (len f) & len f <= len g )
A173: len g = (len g1) + (len g2) by FINSEQ_1:22;
j2 + 1 <= i2 by A59, NAT_1:13;
then A174: 1 <= l by XREAL_1:19;
then A175: l in dom g2 by A74, FINSEQ_1:1;
hence g /. (len g) = g2 /. l by A73, A173, FINSEQ_4:69
.= G * (i1,m1) by A73, A74, A175
.= f /. (len f) by A3, A46, A58 ;
::_thesis: len f <= len g
thus len f <= len g by A3, A23, A39, A73, A174, A173, XREAL_1:7; ::_thesis: verum
end;
case i2 = j2 ; ::_thesis: contradiction
hence contradiction by A6, A17, A19, A44, A46, A58; ::_thesis: verum
end;
caseA176: i2 < j2 ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st
( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
set lk = { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= w `2 & w `2 <= (G * (i1,j2)) `2 ) } ;
A177: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;
reconsider l = j2 - i2 as Element of NAT by A176, INT_1:5;
deffunc H1( Nat) -> Element of the carrier of (TOP-REAL 2) = G * (i1,(i2 + $1));
consider g2 being FinSequence of (TOP-REAL 2) such that
A178: ( len g2 = l & ( for n being Nat st n in dom g2 holds
g2 /. n = H1(n) ) ) from FINSEQ_4:sch_2();
take g = g1 ^ g2; ::_thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
A179: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_Seg_l_holds_
(_i2_+_n_in_Seg_(width_G)_&_[i1,(i2_+_n)]_in_Indices_G_)
let n be Element of NAT ; ::_thesis: ( n in Seg l implies ( i2 + n in Seg (width G) & [i1,(i2 + n)] in Indices G ) )
A180: n <= i2 + n by NAT_1:11;
assume A181: n in Seg l ; ::_thesis: ( i2 + n in Seg (width G) & [i1,(i2 + n)] in Indices G )
then n <= l by FINSEQ_1:1;
then A182: i2 + n <= l + i2 by XREAL_1:7;
j2 <= width G by A56, FINSEQ_1:1;
then A183: i2 + n <= width G by A182, XXREAL_0:2;
1 <= n by A181, FINSEQ_1:1;
then 1 <= i2 + n by A180, XXREAL_0:2;
hence i2 + n in Seg (width G) by A183, FINSEQ_1:1; ::_thesis: [i1,(i2 + n)] in Indices G
hence [i1,(i2 + n)] in Indices G by A47, A49, ZFMISC_1:87; ::_thesis: verum
end;
A184: dom g2 = Seg (len g2) by FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_holds_
ex_m_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_
(_[m,k]_in_Indices_G_&_g2_/._n_=_G_*_(m,k)_)
let n be Element of NAT ; ::_thesis: ( n in dom g2 implies ex m being Element of NAT ex k being Element of NAT st
( [m,k] in Indices G & g2 /. n = G * (m,k) ) )
assume A185: n in dom g2 ; ::_thesis: ex m being Element of NAT ex k being Element of NAT st
( [m,k] in Indices G & g2 /. n = G * (m,k) )
take m = i1; ::_thesis: ex k being Element of NAT st
( [m,k] in Indices G & g2 /. n = G * (m,k) )
take k = i2 + n; ::_thesis: ( [m,k] in Indices G & g2 /. n = G * (m,k) )
thus ( [m,k] in Indices G & g2 /. n = G * (m,k) ) by A178, A179, A184, A185; ::_thesis: verum
end;
then A186: for n being Element of NAT st n in dom g holds
ex i, j being Element of NAT st
( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;
A187: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_&_n_+_1_in_dom_g2_holds_
for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g2_/._n_=_G_*_(l1,l2)_&_g2_/._(n_+_1)_=_G_*_(l3,l4)_holds_
(abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds
(abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A188: n in dom g2 and
A189: n + 1 in dom g2 ; ::_thesis: for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds
(abs (l1 - l3)) + (abs (l2 - l4)) = 1
let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A190: [l1,l2] in Indices G and
A191: [l3,l4] in Indices G and
A192: g2 /. n = G * (l1,l2) and
A193: g2 /. (n + 1) = G * (l3,l4) ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1
( g2 /. (n + 1) = G * (i1,(i2 + (n + 1))) & [i1,(i2 + (n + 1))] in Indices G ) by A178, A179, A184, A189;
then A194: ( l3 = i1 & l4 = i2 + (n + 1) ) by A191, A193, GOBOARD1:5;
( g2 /. n = G * (i1,(i2 + n)) & [i1,(i2 + n)] in Indices G ) by A178, A179, A184, A188;
then ( l1 = i1 & l2 = i2 + n ) by A190, A192, GOBOARD1:5;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs ((i2 + n) - (i2 + (n + 1)))) by A194, ABSVALUE:2
.= abs (- 1)
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
now__::_thesis:_for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g1_/._(len_g1)_=_G_*_(l1,l2)_&_g2_/._1_=_G_*_(l3,l4)_&_len_g1_in_dom_g1_&_1_in_dom_g2_holds_
(abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1
let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A195: [l1,l2] in Indices G and
A196: [l3,l4] in Indices G and
A197: g1 /. (len g1) = G * (l1,l2) and
A198: g2 /. 1 = G * (l3,l4) and
len g1 in dom g1 and
A199: 1 in dom g2 ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1
( g2 /. 1 = G * (i1,(i2 + 1)) & [i1,(i2 + 1)] in Indices G ) by A178, A179, A184, A199;
then A200: ( l3 = i1 & l4 = i2 + 1 ) by A196, A198, GOBOARD1:5;
(f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71;
then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A195, A197, GOBOARD1:5;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = 0 + (abs (i2 - (i2 + 1))) by A200, ABSVALUE:2
.= abs ((i2 - i2) + (- 1))
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
then for n being Element of NAT st n in dom g & n + 1 in dom g holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A41, A187, GOBOARD1:24;
hence g is_sequence_on G by A186, GOBOARD1:def_9; ::_thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
A201: G * (i1,j2) = |[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| by EUCLID:53;
j2 in dom l1 by A56, A55, FINSEQ_1:def_3;
then l1 /. j2 = l1 . j2 by PARTFUN1:def_6;
then A202: l1 /. j2 = G * (i1,j2) by A56, MATRIX_1:def_7;
then A203: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, GOBOARD1:def_2;
i2 in dom l1 by A51, A55, FINSEQ_1:def_3;
then l1 /. i2 = l1 . i2 by PARTFUN1:def_6;
then A204: l1 /. i2 = G * (i1,i2) by A51, MATRIX_1:def_7;
then A205: (Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, GOBOARD1:def_2;
then A206: (G * (i1,i2)) `2 < (G * (i1,j2)) `2 by A51, A56, A54, A20, A55, A176, A203, SEQM_3:def_1;
A207: (X_axis l1) . j2 = (G * (i1,j2)) `1 by A56, A42, A55, A202, GOBOARD1:def_1;
(X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A204, GOBOARD1:def_1;
then A208: (G * (i1,i2)) `1 = (G * (i1,j2)) `1 by A51, A56, A50, A42, A55, A207, SEQM_3:def_10;
A209: LSeg (f,k) = LSeg ((G * (i1,i2)),(G * (i1,j2))) by A3, A13, A19, A46, A58, TOPREAL1:def_3
.= { w where w is Point of (TOP-REAL 2) : ( w `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= w `2 & w `2 <= (G * (i1,j2)) `2 ) } by A206, A208, A177, A201, TOPREAL3:9 ;
A210: dom g2 = Seg l by A178, FINSEQ_1:def_3;
thus L~ g = L~ f ::_thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
proof
set lg = { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ;
set lf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
A211: len g = (len g1) + (len g2) by FINSEQ_1:22;
A212: now__::_thesis:_for_j_being_Element_of_NAT_st_len_g1_<=_j_&_j_<=_len_g_holds_
for_p_being_Point_of_(TOP-REAL_2)_st_p_=_g_/._j_holds_
(_p_`1_=_(G_*_(i1,i2))_`1_&_(G_*_(i1,i2))_`2_<=_p_`2_&_p_`2_<=_(G_*_(i1,j2))_`2_&_p_in_rng_l1_)
let j be Element of NAT ; ::_thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds
( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) )
assume that
A213: len g1 <= j and
A214: j <= len g ; ::_thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds
( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )
reconsider w = j - (len g1) as Element of NAT by A213, INT_1:5;
let p be Point of (TOP-REAL 2); ::_thesis: ( p = g /. j implies ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) )
assume A215: p = g /. j ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )
set u = i2 + w;
A216: dom l1 = Seg (len l1) by FINSEQ_1:def_3;
now__::_thesis:_(_p_`1_=_(G_*_(i1,i2))_`1_&_(G_*_(i1,i2))_`2_<=_p_`2_&_p_`2_<=_(G_*_(i1,j2))_`2_&_p_in_rng_l1_)
percases ( j = len g1 or j <> len g1 ) ;
supposeA217: j = len g1 ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then A218: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68
.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;
hence p `1 = (G * (i1,i2)) `1 by A215, A217; ::_thesis: ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )
thus ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 ) by A51, A56, A54, A20, A55, A176, A205, A203, A215, A217, A218, SEQM_3:def_1; ::_thesis: p in rng l1
thus p in rng l1 by A51, A55, A204, A215, A216, A217, A218, PARTFUN2:2; ::_thesis: verum
end;
supposeA219: j <> len g1 ; ::_thesis: ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )
A220: w + (len g1) = j ;
then A221: w <= len g2 by A211, A214, XREAL_1:6;
A222: (X_axis l1) . i2 = (G * (i1,i2)) `1 by A51, A42, A55, A204, GOBOARD1:def_1;
A223: j - (len g1) <> 0 by A219;
then A224: w >= 1 by NAT_1:14;
then A225: g /. j = g2 /. w by A220, A221, SEQ_4:136;
A226: i2 < i2 + w by A223, XREAL_1:29;
A227: w in dom g2 by A224, A221, FINSEQ_3:25;
then A228: i2 + w in Seg (width G) by A210, A179;
i2 + w in Seg (width G) by A210, A179, A227;
then i2 + w in dom l1 by A55, FINSEQ_1:def_3;
then l1 /. (i2 + w) = l1 . (i2 + w) by PARTFUN1:def_6;
then A229: l1 /. (i2 + w) = G * (i1,(i2 + w)) by A228, MATRIX_1:def_7;
then A230: (Y_axis l1) . (i2 + w) = (G * (i1,(i2 + w))) `2 by A20, A55, A228, GOBOARD1:def_2;
A231: g2 /. w = G * (i1,(i2 + w)) by A178, A227;
(X_axis l1) . (i2 + w) = (G * (i1,(i2 + w))) `1 by A42, A55, A228, A229, GOBOARD1:def_1;
hence p `1 = (G * (i1,i2)) `1 by A51, A50, A42, A55, A215, A225, A231, A228, A222, SEQM_3:def_10; ::_thesis: ( (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 )
(Y_axis l1) . i2 = (G * (i1,i2)) `2 by A51, A20, A55, A204, GOBOARD1:def_2;
hence (G * (i1,i2)) `2 <= p `2 by A51, A54, A20, A55, A215, A225, A231, A228, A230, A226, SEQM_3:def_1; ::_thesis: ( p `2 <= (G * (i1,j2)) `2 & p in rng l1 )
A232: (Y_axis l1) . j2 = (G * (i1,j2)) `2 by A56, A20, A55, A202, GOBOARD1:def_2;
now__::_thesis:_p_`2_<=_(G_*_(i1,j2))_`2
percases ( i2 + w = j2 or i2 + w <> j2 ) ;
suppose i2 + w = j2 ; ::_thesis: p `2 <= (G * (i1,j2)) `2
hence p `2 <= (G * (i1,j2)) `2 by A215, A224, A220, A221, A231, SEQ_4:136; ::_thesis: verum
end;
supposeA233: i2 + w <> j2 ; ::_thesis: p `2 <= (G * (i1,j2)) `2
i2 + w <= i2 + l by A178, A221, XREAL_1:7;
then i2 + w < j2 by A233, XXREAL_0:1;
hence p `2 <= (G * (i1,j2)) `2 by A56, A54, A20, A55, A215, A225, A231, A228, A230, A232, SEQM_3:def_1; ::_thesis: verum
end;
end;
end;
hence p `2 <= (G * (i1,j2)) `2 ; ::_thesis: p in rng l1
thus p in rng l1 by A55, A215, A216, A225, A231, A228, A229, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
hence ( p `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= p `2 & p `2 <= (G * (i1,j2)) `2 & p in rng l1 ) ; ::_thesis: verum
end;
thus L~ g c= L~ f :: according to XBOOLE_0:def_10 ::_thesis: L~ f c= L~ g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ g or x in L~ f )
assume x in L~ g ; ::_thesis: x in L~ f
then consider X being set such that
A234: x in X and
A235: X in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def_4;
consider i being Element of NAT such that
A236: X = LSeg (g,i) and
A237: 1 <= i and
A238: i + 1 <= len g by A235;
now__::_thesis:_x_in_L~_f
percases ( i + 1 <= len g1 or i + 1 > len g1 ) ;
supposeA239: i + 1 <= len g1 ; ::_thesis: x in L~ f
i <= i + 1 by NAT_1:11;
then i <= len g1 by A239, XXREAL_0:2;
then A240: i in dom g1 by A237, FINSEQ_3:25;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom g1 by A239, FINSEQ_3:25;
then X = LSeg (g1,i) by A236, A240, TOPREAL3:18;
then X in { (LSeg (g1,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A237, A239;
then A241: x in L~ (f | k) by A36, A234, TARSKI:def_4;
L~ (f | k) c= L~ f by TOPREAL3:20;
hence x in L~ f by A241; ::_thesis: verum
end;
supposeA242: i + 1 > len g1 ; ::_thesis: x in L~ f
reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;
A243: i <= len g by A238, NAT_1:13;
A244: len g1 <= i by A242, NAT_1:13;
then A245: q1 `1 = (G * (i1,i2)) `1 by A212, A243;
A246: q1 `2 <= (G * (i1,j2)) `2 by A212, A244, A243;
A247: (G * (i1,i2)) `2 <= q1 `2 by A212, A244, A243;
q2 `1 = (G * (i1,i2)) `1 by A212, A238, A242;
then A248: q2 = |[(q1 `1),(q2 `2)]| by A245, EUCLID:53;
A249: q2 `2 <= (G * (i1,j2)) `2 by A212, A238, A242;
A250: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A237, A238, EUCLID:53, TOPREAL1:def_3;
A251: (G * (i1,i2)) `2 <= q2 `2 by A212, A238, A242;
now__::_thesis:_x_in_L~_f
percases ( q1 `2 > q2 `2 or q1 `2 = q2 `2 or q1 `2 < q2 `2 ) by XXREAL_0:1;
suppose q1 `2 > q2 `2 ; ::_thesis: x in L~ f
then LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q1 `1 & q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) } by A248, A250, TOPREAL3:9;
then consider p2 being Point of (TOP-REAL 2) such that
A252: ( p2 = x & p2 `1 = q1 `1 ) and
A253: ( q2 `2 <= p2 `2 & p2 `2 <= q1 `2 ) by A234, A236;
( (G * (i1,i2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,j2)) `2 ) by A246, A251, A253, XXREAL_0:2;
then A254: x in LSeg (f,k) by A209, A245, A252;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A254, TARSKI:def_4; ::_thesis: verum
end;
suppose q1 `2 = q2 `2 ; ::_thesis: x in L~ f
then LSeg (g,i) = {q1} by A248, A250, RLTOPSP1:70;
then x = q1 by A234, A236, TARSKI:def_1;
then A255: x in LSeg (f,k) by A209, A245, A247, A246;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A255, TARSKI:def_4; ::_thesis: verum
end;
suppose q1 `2 < q2 `2 ; ::_thesis: x in L~ f
then LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = q1 `1 & q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) } by A248, A250, TOPREAL3:9;
then consider p2 being Point of (TOP-REAL 2) such that
A256: ( p2 = x & p2 `1 = q1 `1 ) and
A257: ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A234, A236;
( (G * (i1,i2)) `2 <= p2 `2 & p2 `2 <= (G * (i1,j2)) `2 ) by A247, A249, A257, XXREAL_0:2;
then A258: x in LSeg (f,k) by A209, A245, A256;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A258, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in L~ f ; ::_thesis: verum
end;
end;
end;
hence x in L~ f ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in L~ g )
assume x in L~ f ; ::_thesis: x in L~ g
then A259: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3;
now__::_thesis:_x_in_L~_g
percases ( x in L~ (f | k) or x in LSeg (f,k) ) by A259, XBOOLE_0:def_3;
supposeA260: x in L~ (f | k) ; ::_thesis: x in L~ g
L~ g1 c= L~ g by Th6;
hence x in L~ g by A36, A260; ::_thesis: verum
end;
suppose x in LSeg (f,k) ; ::_thesis: x in L~ g
then consider p1 being Point of (TOP-REAL 2) such that
A261: p1 = x and
A262: p1 `1 = (G * (i1,i2)) `1 and
A263: (G * (i1,i2)) `2 <= p1 `2 and
A264: p1 `2 <= (G * (i1,j2)) `2 by A209;
defpred S2[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds
q `2 <= p1 `2 ) );
A265: now__::_thesis:_ex_n_being_Nat_st_S2[n]
reconsider n = len g1 as Nat ;
take n = n; ::_thesis: S2[n]
thus S2[n] ::_thesis: verum
proof
thus ( len g1 <= n & n <= len g ) by A211, XREAL_1:31; ::_thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds
q `2 <= p1 `2
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then A266: len g1 in dom g1 by FINSEQ_3:25;
let q be Point of (TOP-REAL 2); ::_thesis: ( q = g /. n implies q `2 <= p1 `2 )
assume q = g /. n ; ::_thesis: q `2 <= p1 `2
then q = (f | k) /. (len (f | k)) by A38, A266, FINSEQ_4:68
.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;
hence q `2 <= p1 `2 by A263; ::_thesis: verum
end;
end;
A267: for n being Nat st S2[n] holds
n <= len g ;
consider ma being Nat such that
A268: ( S2[ma] & ( for n being Nat st S2[n] holds
n <= ma ) ) from NAT_1:sch_6(A267, A265);
reconsider ma = ma as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_x_in_L~_g
percases ( ma = len g or ma <> len g ) ;
supposeA269: ma = len g ; ::_thesis: x in L~ g
i2 + 1 <= j2 by A176, NAT_1:13;
then A270: 1 <= l by XREAL_1:19;
then 0 + 1 <= ma by A178, A211, A269, XREAL_1:7;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;
A271: m1 + 1 = ma ;
(len g1) + 1 <= ma by A178, A211, A269, A270, XREAL_1:7;
then A272: m1 >= len g1 by A271, XREAL_1:6;
reconsider q = g /. m1 as Point of (TOP-REAL 2) ;
set lq = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & q `2 <= e `2 & e `2 <= (G * (i1,j2)) `2 ) } ;
A273: i2 + l = j2 ;
A274: l in dom g2 by A178, A270, FINSEQ_3:25;
then A275: g /. ma = g2 /. l by A178, A211, A269, FINSEQ_4:69
.= G * (i1,j2) by A178, A274, A273 ;
then (G * (i1,j2)) `2 <= p1 `2 by A268;
then A276: p1 `2 = (G * (i1,j2)) `2 by A264, XXREAL_0:1;
A277: m1 <= len g by A269, A271, NAT_1:11;
then A278: q `1 = (G * (i1,i2)) `1 by A212, A272;
A279: q `2 <= (G * (i1,j2)) `2 by A212, A272, A277;
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then A280: 1 <= m1 by A272, XXREAL_0:2;
then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (i1,j2)),q) ) by A269, A275, A271, EUCLID:53, TOPREAL1:def_3;
then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `1 = (G * (i1,i2)) `1 & q `2 <= e `2 & e `2 <= (G * (i1,j2)) `2 ) } by A208, A201, A278, A279, TOPREAL3:9;
then A281: p1 in LSeg (g,m1) by A262, A276, A279;
LSeg (g,m1) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A269, A271, A280;
hence x in L~ g by A261, A281, TARSKI:def_4; ::_thesis: verum
end;
suppose ma <> len g ; ::_thesis: x in L~ g
then ma < len g by A268, XXREAL_0:1;
then A282: ma + 1 <= len g by NAT_1:13;
reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;
set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa `2 <= p2 `2 & p2 `2 <= qa1 `2 ) } ;
A283: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53;
A284: qa `2 <= p1 `2 by A268;
A285: len g1 <= ma + 1 by A268, NAT_1:13;
then A286: qa1 `1 = (G * (i1,i2)) `1 by A212, A282;
A287: now__::_thesis:_not_qa1_`2_<=_p1_`2
assume qa1 `2 <= p1 `2 ; ::_thesis: contradiction
then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds
q `2 <= p1 `2 ;
then ma + 1 <= ma by A268, A282, A285;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
A288: ( qa `1 = (G * (i1,i2)) `1 & qa = |[(qa `1),(qa `2)]| ) by A212, A268, EUCLID:53;
A289: 1 <= ma by A13, A23, A39, A268, NAT_1:13;
then LSeg (g,ma) = LSeg (qa,qa1) by A282, TOPREAL1:def_3
.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = (G * (i1,i2)) `1 & qa `2 <= p2 `2 & p2 `2 <= qa1 `2 ) } by A284, A287, A286, A288, A283, TOPREAL3:9, XXREAL_0:2 ;
then A290: x in LSeg (g,ma) by A261, A262, A284, A287;
LSeg (g,ma) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A289, A282;
hence x in L~ g by A290, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in L~ g ; ::_thesis: verum
end;
end;
end;
hence x in L~ g ; ::_thesis: verum
end;
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:25;
hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68
.= f /. 1 by A17, A15, FINSEQ_4:71 ;
::_thesis: ( g /. (len g) = f /. (len f) & len f <= len g )
A291: len g = (len g1) + l by A178, FINSEQ_1:22;
i2 + 1 <= j2 by A176, NAT_1:13;
then A292: 1 <= l by XREAL_1:19;
then A293: l in dom g2 by A178, A184, FINSEQ_1:1;
hence g /. (len g) = g2 /. l by A291, FINSEQ_4:69
.= G * (i1,(i2 + l)) by A178, A293
.= f /. (len f) by A3, A46, A58 ;
::_thesis: len f <= len g
thus len f <= len g by A3, A23, A39, A292, A291, XREAL_1:7; ::_thesis: verum
end;
end;
end;
hence ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; ::_thesis: verum
end;
supposeA294: i2 = j2 ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
set ppi = G * (i1,i2);
set pj = G * (j1,i2);
now__::_thesis:_(_(_i1_>_j1_&_ex_g_being_FinSequence_of_the_carrier_of_(TOP-REAL_2)_st_
(_g_is_sequence_on_G_&_L~_g_=_L~_f_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_)_)_or_(_i1_=_j1_&_contradiction_)_or_(_i1_<_j1_&_ex_g_being_FinSequence_of_the_carrier_of_(TOP-REAL_2)_st_
(_g_is_sequence_on_G_&_L~_g_=_L~_f_&_g_/._1_=_f_/._1_&_g_/._(len_g)_=_f_/._(len_f)_&_len_f_<=_len_g_)_)_)
percases ( i1 > j1 or i1 = j1 or i1 < j1 ) by XXREAL_0:1;
caseA295: i1 > j1 ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st
( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
c1 /. j1 = c1 . j1 by A48, A43, PARTFUN1:def_6;
then A296: c1 /. j1 = G * (j1,i2) by A48, MATRIX_1:def_8;
then A297: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, GOBOARD1:def_1;
c1 /. i1 = c1 . i1 by A49, A43, PARTFUN1:def_6;
then A298: c1 /. i1 = G * (i1,i2) by A49, MATRIX_1:def_8;
then A299: (X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, GOBOARD1:def_1;
then A300: (G * (j1,i2)) `1 < (G * (i1,i2)) `1 by A49, A48, A52, A43, A22, A295, A297, SEQM_3:def_1;
A301: (Y_axis c1) . j1 = (G * (j1,i2)) `2 by A48, A43, A21, A296, GOBOARD1:def_2;
(Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A298, GOBOARD1:def_2;
then A302: (G * (i1,i2)) `2 = (G * (j1,i2)) `2 by A49, A48, A53, A43, A21, A301, SEQM_3:def_10;
reconsider l = i1 - j1 as Element of NAT by A295, INT_1:5;
defpred S2[ Nat, set ] means for m being Element of NAT st m = i1 - $1 holds
$2 = G * (m,i2);
set lk = { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= w `1 & w `1 <= (G * (i1,i2)) `1 ) } ;
A303: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;
A304: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_Seg_l_holds_
(_i1_-_n_is_Element_of_NAT_&_[(i1_-_n),i2]_in_Indices_G_&_i1_-_n_in_dom_G_)
let n be Element of NAT ; ::_thesis: ( n in Seg l implies ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G ) )
assume n in Seg l ; ::_thesis: ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G )
then A305: n <= l by FINSEQ_1:1;
l <= i1 by XREAL_1:43;
then reconsider w = i1 - n as Element of NAT by A305, INT_1:5, XXREAL_0:2;
( i1 - n <= i1 & i1 <= len G ) by A49, FINSEQ_3:25, XREAL_1:43;
then A306: w <= len G by XXREAL_0:2;
A307: 1 <= j1 by A48, FINSEQ_3:25;
i1 - l <= i1 - n by A305, XREAL_1:13;
then 1 <= w by A307, XXREAL_0:2;
then w in dom G by A306, FINSEQ_3:25;
hence ( i1 - n is Element of NAT & [(i1 - n),i2] in Indices G & i1 - n in dom G ) by A47, A51, ZFMISC_1:87; ::_thesis: verum
end;
A308: now__::_thesis:_for_n_being_Nat_st_n_in_Seg_l_holds_
ex_p_being_Element_of_the_carrier_of_(TOP-REAL_2)_st_S2[n,p]
let n be Nat; ::_thesis: ( n in Seg l implies ex p being Element of the carrier of (TOP-REAL 2) st S2[n,p] )
assume n in Seg l ; ::_thesis: ex p being Element of the carrier of (TOP-REAL 2) st S2[n,p]
then reconsider m = i1 - n as Element of NAT by A304;
take p = G * (m,i2); ::_thesis: S2[n,p]
thus S2[n,p] ; ::_thesis: verum
end;
consider g2 being FinSequence of (TOP-REAL 2) such that
A309: ( len g2 = l & ( for n being Nat st n in Seg l holds
S2[n,g2 /. n] ) ) from FINSEQ_4:sch_1(A308);
take g = g1 ^ g2; ::_thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
A310: dom g2 = Seg l by A309, FINSEQ_1:def_3;
A311: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_&_n_+_1_in_dom_g2_holds_
for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g2_/._n_=_G_*_(l1,l2)_&_g2_/._(n_+_1)_=_G_*_(l3,l4)_holds_
(abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds
(abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A312: n in dom g2 and
A313: n + 1 in dom g2 ; ::_thesis: for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds
(abs (l1 - l3)) + (abs (l2 - l4)) = 1
reconsider m1 = i1 - n, m2 = i1 - (n + 1) as Element of NAT by A304, A310, A312, A313;
let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A314: [l1,l2] in Indices G and
A315: [l3,l4] in Indices G and
A316: g2 /. n = G * (l1,l2) and
A317: g2 /. (n + 1) = G * (l3,l4) ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1
( [(i1 - (n + 1)),i2] in Indices G & g2 /. (n + 1) = G * (m2,i2) ) by A304, A309, A310, A313;
then A318: ( l3 = m2 & l4 = i2 ) by A315, A317, GOBOARD1:5;
( [(i1 - n),i2] in Indices G & g2 /. n = G * (m1,i2) ) by A304, A309, A310, A312;
then ( l1 = m1 & l2 = i2 ) by A314, A316, GOBOARD1:5;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs ((i1 - n) - (i1 - (n + 1)))) + 0 by A318, ABSVALUE:2
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_holds_
ex_m,_k_being_Element_of_NAT_st_
(_[m,k]_in_Indices_G_&_g2_/._n_=_G_*_(m,k)_)
let n be Element of NAT ; ::_thesis: ( n in dom g2 implies ex m, k being Element of NAT st
( [m,k] in Indices G & g2 /. n = G * (m,k) ) )
assume A319: n in dom g2 ; ::_thesis: ex m, k being Element of NAT st
( [m,k] in Indices G & g2 /. n = G * (m,k) )
then reconsider m = i1 - n as Element of NAT by A304, A310;
take m = m; ::_thesis: ex k being Element of NAT st
( [m,k] in Indices G & g2 /. n = G * (m,k) )
take k = i2; ::_thesis: ( [m,k] in Indices G & g2 /. n = G * (m,k) )
thus ( [m,k] in Indices G & g2 /. n = G * (m,k) ) by A304, A309, A310, A319; ::_thesis: verum
end;
then A320: for n being Element of NAT st n in dom g holds
ex i, j being Element of NAT st
( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;
now__::_thesis:_for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g1_/._(len_g1)_=_G_*_(l1,l2)_&_g2_/._1_=_G_*_(l3,l4)_&_len_g1_in_dom_g1_&_1_in_dom_g2_holds_
(abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1
let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A321: [l1,l2] in Indices G and
A322: [l3,l4] in Indices G and
A323: g1 /. (len g1) = G * (l1,l2) and
A324: g2 /. 1 = G * (l3,l4) and
len g1 in dom g1 and
A325: 1 in dom g2 ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1
reconsider m1 = i1 - 1 as Element of NAT by A304, A310, A325;
( [(i1 - 1),i2] in Indices G & g2 /. 1 = G * (m1,i2) ) by A304, A309, A310, A325;
then A326: ( l3 = m1 & l4 = i2 ) by A322, A324, GOBOARD1:5;
(f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71;
then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A321, A323, GOBOARD1:5;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs (i1 - (i1 - 1))) + 0 by A326, ABSVALUE:2
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
then for n being Element of NAT st n in dom g & n + 1 in dom g holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A41, A311, GOBOARD1:24;
hence g is_sequence_on G by A320, GOBOARD1:def_9; ::_thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
reconsider m1 = i1 - l as Element of NAT ;
A327: G * (j1,i2) = |[((G * (j1,i2)) `1),((G * (j1,i2)) `2)]| by EUCLID:53;
A328: LSeg (f,k) = LSeg ((G * (j1,i2)),(G * (i1,i2))) by A3, A13, A19, A46, A294, TOPREAL1:def_3
.= { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= w `1 & w `1 <= (G * (i1,i2)) `1 ) } by A300, A302, A303, A327, TOPREAL3:10 ;
thus L~ g = L~ f ::_thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
proof
set lg = { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ;
set lf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
A329: len g = (len g1) + (len g2) by FINSEQ_1:22;
A330: now__::_thesis:_for_j_being_Element_of_NAT_st_len_g1_<=_j_&_j_<=_len_g_holds_
for_p_being_Point_of_(TOP-REAL_2)_st_p_=_g_/._j_holds_
(_p_`2_=_(G_*_(i1,i2))_`2_&_(G_*_(j1,i2))_`1_<=_p_`1_&_p_`1_<=_(G_*_(i1,i2))_`1_&_p_in_rng_c1_)
let j be Element of NAT ; ::_thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds
( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) )
assume that
A331: len g1 <= j and
A332: j <= len g ; ::_thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds
( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )
reconsider w = j - (len g1) as Element of NAT by A331, INT_1:5;
let p be Point of (TOP-REAL 2); ::_thesis: ( p = g /. j implies ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) )
assume A333: p = g /. j ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )
now__::_thesis:_(_p_`2_=_(G_*_(i1,i2))_`2_&_(G_*_(j1,i2))_`1_<=_p_`1_&_p_`1_<=_(G_*_(i1,i2))_`1_&_p_in_rng_c1_)
percases ( j = len g1 or j <> len g1 ) ;
supposeA334: j = len g1 ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then A335: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68
.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;
hence p `2 = (G * (i1,i2)) `2 by A333, A334; ::_thesis: ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )
thus ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 ) by A49, A48, A52, A43, A22, A295, A299, A297, A333, A334, A335, SEQM_3:def_1; ::_thesis: p in rng c1
thus p in rng c1 by A49, A43, A298, A333, A334, A335, PARTFUN2:2; ::_thesis: verum
end;
supposeA336: j <> len g1 ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )
A337: w + (len g1) = j ;
then A338: w <= len g2 by A329, A332, XREAL_1:6;
A339: j - (len g1) <> 0 by A336;
then A340: w >= 1 by NAT_1:14;
then A341: w in dom g2 by A338, FINSEQ_3:25;
then reconsider u = i1 - w as Element of NAT by A304, A310;
A342: g /. j = g2 /. w by A340, A337, A338, SEQ_4:136;
A343: u < i1 by A339, XREAL_1:44;
A344: g2 /. w = G * (u,i2) by A309, A310, A341;
A345: (Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A298, GOBOARD1:def_2;
A346: i1 - w in dom G by A304, A310, A341;
c1 /. u = c1 . u by A43, A304, A310, A341, PARTFUN1:def_6;
then A347: c1 /. u = G * (u,i2) by A346, MATRIX_1:def_8;
then A348: (X_axis c1) . u = (G * (u,i2)) `1 by A43, A22, A346, GOBOARD1:def_1;
(Y_axis c1) . u = (G * (u,i2)) `2 by A43, A21, A346, A347, GOBOARD1:def_2;
hence p `2 = (G * (i1,i2)) `2 by A49, A53, A43, A21, A333, A342, A346, A344, A345, SEQM_3:def_10; ::_thesis: ( (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 )
A349: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, A296, GOBOARD1:def_1;
now__::_thesis:_(G_*_(j1,i2))_`1_<=_p_`1
percases ( u = j1 or u <> j1 ) ;
suppose u = j1 ; ::_thesis: (G * (j1,i2)) `1 <= p `1
hence (G * (j1,i2)) `1 <= p `1 by A333, A340, A337, A338, A344, SEQ_4:136; ::_thesis: verum
end;
supposeA350: u <> j1 ; ::_thesis: (G * (j1,i2)) `1 <= p `1
i1 - (len g2) <= u by A338, XREAL_1:13;
then j1 < u by A309, A350, XXREAL_0:1;
hence (G * (j1,i2)) `1 <= p `1 by A48, A52, A43, A22, A333, A342, A346, A344, A348, A349, SEQM_3:def_1; ::_thesis: verum
end;
end;
end;
hence (G * (j1,i2)) `1 <= p `1 ; ::_thesis: ( p `1 <= (G * (i1,i2)) `1 & p in rng c1 )
(X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, A298, GOBOARD1:def_1;
hence p `1 <= (G * (i1,i2)) `1 by A49, A52, A43, A22, A333, A342, A346, A344, A348, A343, SEQM_3:def_1; ::_thesis: p in rng c1
thus p in rng c1 by A43, A333, A342, A346, A344, A347, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
hence ( p `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= p `1 & p `1 <= (G * (i1,i2)) `1 & p in rng c1 ) ; ::_thesis: verum
end;
thus L~ g c= L~ f :: according to XBOOLE_0:def_10 ::_thesis: L~ f c= L~ g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ g or x in L~ f )
assume x in L~ g ; ::_thesis: x in L~ f
then consider X being set such that
A351: x in X and
A352: X in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def_4;
consider i being Element of NAT such that
A353: X = LSeg (g,i) and
A354: 1 <= i and
A355: i + 1 <= len g by A352;
now__::_thesis:_x_in_L~_f
percases ( i + 1 <= len g1 or i + 1 > len g1 ) ;
supposeA356: i + 1 <= len g1 ; ::_thesis: x in L~ f
i <= i + 1 by NAT_1:11;
then i <= len g1 by A356, XXREAL_0:2;
then A357: i in dom g1 by A354, FINSEQ_3:25;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom g1 by A356, FINSEQ_3:25;
then X = LSeg (g1,i) by A353, A357, TOPREAL3:18;
then X in { (LSeg (g1,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A354, A356;
then A358: x in L~ (f | k) by A36, A351, TARSKI:def_4;
L~ (f | k) c= L~ f by TOPREAL3:20;
hence x in L~ f by A358; ::_thesis: verum
end;
supposeA359: i + 1 > len g1 ; ::_thesis: x in L~ f
reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;
A360: i <= len g by A355, NAT_1:13;
A361: len g1 <= i by A359, NAT_1:13;
then A362: q1 `2 = (G * (i1,i2)) `2 by A330, A360;
A363: q1 `1 <= (G * (i1,i2)) `1 by A330, A361, A360;
A364: (G * (j1,i2)) `1 <= q1 `1 by A330, A361, A360;
q2 `2 = (G * (i1,i2)) `2 by A330, A355, A359;
then A365: q2 = |[(q2 `1),(q1 `2)]| by A362, EUCLID:53;
A366: q2 `1 <= (G * (i1,i2)) `1 by A330, A355, A359;
A367: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A354, A355, EUCLID:53, TOPREAL1:def_3;
A368: (G * (j1,i2)) `1 <= q2 `1 by A330, A355, A359;
now__::_thesis:_x_in_L~_f
percases ( q1 `1 > q2 `1 or q1 `1 = q2 `1 or q1 `1 < q2 `1 ) by XXREAL_0:1;
suppose q1 `1 > q2 `1 ; ::_thesis: x in L~ f
then LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q1 `2 & q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) } by A365, A367, TOPREAL3:10;
then consider p2 being Point of (TOP-REAL 2) such that
A369: ( p2 = x & p2 `2 = q1 `2 ) and
A370: ( q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) by A351, A353;
( (G * (j1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (i1,i2)) `1 ) by A363, A368, A370, XXREAL_0:2;
then A371: x in LSeg (f,k) by A328, A362, A369;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A371, TARSKI:def_4; ::_thesis: verum
end;
suppose q1 `1 = q2 `1 ; ::_thesis: x in L~ f
then LSeg (g,i) = {q1} by A365, A367, RLTOPSP1:70;
then x = q1 by A351, A353, TARSKI:def_1;
then A372: x in LSeg (f,k) by A328, A362, A364, A363;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A372, TARSKI:def_4; ::_thesis: verum
end;
suppose q1 `1 < q2 `1 ; ::_thesis: x in L~ f
then LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = q1 `2 & q1 `1 <= p1 `1 & p1 `1 <= q2 `1 ) } by A365, A367, TOPREAL3:10;
then consider p2 being Point of (TOP-REAL 2) such that
A373: ( p2 = x & p2 `2 = q1 `2 ) and
A374: ( q1 `1 <= p2 `1 & p2 `1 <= q2 `1 ) by A351, A353;
( (G * (j1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (i1,i2)) `1 ) by A364, A366, A374, XXREAL_0:2;
then A375: x in LSeg (f,k) by A328, A362, A373;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A375, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in L~ f ; ::_thesis: verum
end;
end;
end;
hence x in L~ f ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in L~ g )
assume x in L~ f ; ::_thesis: x in L~ g
then A376: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3;
now__::_thesis:_x_in_L~_g
percases ( x in L~ (f | k) or x in LSeg (f,k) ) by A376, XBOOLE_0:def_3;
supposeA377: x in L~ (f | k) ; ::_thesis: x in L~ g
L~ g1 c= L~ g by Th6;
hence x in L~ g by A36, A377; ::_thesis: verum
end;
suppose x in LSeg (f,k) ; ::_thesis: x in L~ g
then consider p1 being Point of (TOP-REAL 2) such that
A378: p1 = x and
A379: p1 `2 = (G * (i1,i2)) `2 and
A380: (G * (j1,i2)) `1 <= p1 `1 and
A381: p1 `1 <= (G * (i1,i2)) `1 by A328;
defpred S3[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds
q `1 >= p1 `1 ) );
A382: now__::_thesis:_ex_n_being_Nat_st_S3[n]
reconsider n = len g1 as Nat ;
take n = n; ::_thesis: S3[n]
thus S3[n] ::_thesis: verum
proof
thus ( len g1 <= n & n <= len g ) by A329, XREAL_1:31; ::_thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds
q `1 >= p1 `1
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then A383: len g1 in dom g1 by FINSEQ_3:25;
let q be Point of (TOP-REAL 2); ::_thesis: ( q = g /. n implies q `1 >= p1 `1 )
assume q = g /. n ; ::_thesis: q `1 >= p1 `1
then q = (f | k) /. (len (f | k)) by A38, A383, FINSEQ_4:68
.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;
hence q `1 >= p1 `1 by A381; ::_thesis: verum
end;
end;
A384: for n being Nat st S3[n] holds
n <= len g ;
consider ma being Nat such that
A385: ( S3[ma] & ( for n being Nat st S3[n] holds
n <= ma ) ) from NAT_1:sch_6(A384, A382);
reconsider ma = ma as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_x_in_L~_g
percases ( ma = len g or ma <> len g ) ;
supposeA386: ma = len g ; ::_thesis: x in L~ g
j1 + 1 <= i1 by A295, NAT_1:13;
then A387: 1 <= l by XREAL_1:19;
then 0 + 1 <= ma by A309, A329, A386, XREAL_1:7;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;
A388: m1 + 1 = ma ;
(len g1) + 1 <= ma by A309, A329, A386, A387, XREAL_1:7;
then A389: m1 >= len g1 by A388, XREAL_1:6;
reconsider q = g /. m1 as Point of (TOP-REAL 2) ;
set lq = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= e `1 & e `1 <= q `1 ) } ;
A390: i1 - l = j1 ;
A391: l in dom g2 by A310, A387, FINSEQ_1:1;
then A392: g /. ma = g2 /. l by A309, A329, A386, FINSEQ_4:69
.= G * (j1,i2) by A309, A310, A391, A390 ;
then p1 `1 <= (G * (j1,i2)) `1 by A385;
then A393: p1 `1 = (G * (j1,i2)) `1 by A380, XXREAL_0:1;
A394: m1 <= len g by A386, A388, NAT_1:11;
then A395: q `2 = (G * (i1,i2)) `2 by A330, A389;
A396: (G * (j1,i2)) `1 <= q `1 by A330, A389, A394;
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then A397: 1 <= m1 by A389, XXREAL_0:2;
then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (j1,i2)),q) ) by A386, A392, A388, EUCLID:53, TOPREAL1:def_3;
then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= e `1 & e `1 <= q `1 ) } by A302, A327, A395, A396, TOPREAL3:10;
then A398: p1 in LSeg (g,m1) by A379, A393, A396;
LSeg (g,m1) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A386, A388, A397;
hence x in L~ g by A378, A398, TARSKI:def_4; ::_thesis: verum
end;
suppose ma <> len g ; ::_thesis: x in L~ g
then ma < len g by A385, XXREAL_0:1;
then A399: ma + 1 <= len g by NAT_1:13;
reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;
set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * (i1,i2)) `2 & qa1 `1 <= p2 `1 & p2 `1 <= qa `1 ) } ;
A400: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53;
A401: p1 `1 <= qa `1 by A385;
A402: len g1 <= ma + 1 by A385, NAT_1:13;
then A403: qa1 `2 = (G * (i1,i2)) `2 by A330, A399;
A404: now__::_thesis:_not_p1_`1_<=_qa1_`1
assume p1 `1 <= qa1 `1 ; ::_thesis: contradiction
then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds
p1 `1 <= q `1 ;
then ma + 1 <= ma by A385, A399, A402;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
A405: ( qa `2 = (G * (i1,i2)) `2 & qa = |[(qa `1),(qa `2)]| ) by A330, A385, EUCLID:53;
A406: 1 <= ma by A13, A23, A39, A385, NAT_1:13;
then LSeg (g,ma) = LSeg (qa1,qa) by A399, TOPREAL1:def_3
.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * (i1,i2)) `2 & qa1 `1 <= p2 `1 & p2 `1 <= qa `1 ) } by A401, A404, A403, A405, A400, TOPREAL3:10, XXREAL_0:2 ;
then A407: x in LSeg (g,ma) by A378, A379, A401, A404;
LSeg (g,ma) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A406, A399;
hence x in L~ g by A407, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in L~ g ; ::_thesis: verum
end;
end;
end;
hence x in L~ g ; ::_thesis: verum
end;
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then 1 in dom g1 by A57, FINSEQ_1:1;
hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68
.= f /. 1 by A17, A15, FINSEQ_4:71 ;
::_thesis: ( g /. (len g) = f /. (len f) & len f <= len g )
A408: len g = (len g1) + (len g2) by FINSEQ_1:22;
j1 + 1 <= i1 by A295, NAT_1:13;
then A409: 1 <= l by XREAL_1:19;
then A410: l in dom g2 by A310, FINSEQ_1:1;
hence g /. (len g) = g2 /. l by A309, A408, FINSEQ_4:69
.= G * (m1,i2) by A309, A310, A410
.= f /. (len f) by A3, A46, A294 ;
::_thesis: len f <= len g
thus len f <= len g by A3, A23, A39, A309, A409, A408, XREAL_1:7; ::_thesis: verum
end;
case i1 = j1 ; ::_thesis: contradiction
hence contradiction by A6, A17, A19, A44, A46, A294; ::_thesis: verum
end;
caseA411: i1 < j1 ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st
( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
set lk = { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= w `1 & w `1 <= (G * (j1,i2)) `1 ) } ;
A412: G * (i1,i2) = |[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| by EUCLID:53;
reconsider l = j1 - i1 as Element of NAT by A411, INT_1:5;
deffunc H1( Nat) -> Element of the carrier of (TOP-REAL 2) = G * ((i1 + $1),i2);
consider g2 being FinSequence of (TOP-REAL 2) such that
A413: ( len g2 = l & ( for n being Nat st n in dom g2 holds
g2 /. n = H1(n) ) ) from FINSEQ_4:sch_2();
take g = g1 ^ g2; ::_thesis: ( g is_sequence_on G & L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
A414: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_Seg_l_holds_
(_i1_+_n_in_dom_G_&_[(i1_+_n),i2]_in_Indices_G_)
let n be Element of NAT ; ::_thesis: ( n in Seg l implies ( i1 + n in dom G & [(i1 + n),i2] in Indices G ) )
A415: n <= i1 + n by NAT_1:11;
assume A416: n in Seg l ; ::_thesis: ( i1 + n in dom G & [(i1 + n),i2] in Indices G )
then n <= l by FINSEQ_1:1;
then A417: i1 + n <= l + i1 by XREAL_1:7;
j1 <= len G by A48, FINSEQ_3:25;
then A418: i1 + n <= len G by A417, XXREAL_0:2;
1 <= n by A416, FINSEQ_1:1;
then 1 <= i1 + n by A415, XXREAL_0:2;
hence i1 + n in dom G by A418, FINSEQ_3:25; ::_thesis: [(i1 + n),i2] in Indices G
hence [(i1 + n),i2] in Indices G by A47, A51, ZFMISC_1:87; ::_thesis: verum
end;
A419: dom g2 = Seg (len g2) by FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_holds_
ex_m_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_
(_[m,k]_in_Indices_G_&_g2_/._n_=_G_*_(m,k)_)
let n be Element of NAT ; ::_thesis: ( n in dom g2 implies ex m being Element of NAT ex k being Element of NAT st
( [m,k] in Indices G & g2 /. n = G * (m,k) ) )
assume A420: n in dom g2 ; ::_thesis: ex m being Element of NAT ex k being Element of NAT st
( [m,k] in Indices G & g2 /. n = G * (m,k) )
take m = i1 + n; ::_thesis: ex k being Element of NAT st
( [m,k] in Indices G & g2 /. n = G * (m,k) )
take k = i2; ::_thesis: ( [m,k] in Indices G & g2 /. n = G * (m,k) )
thus ( [m,k] in Indices G & g2 /. n = G * (m,k) ) by A413, A414, A419, A420; ::_thesis: verum
end;
then A421: for n being Element of NAT st n in dom g holds
ex i, j being Element of NAT st
( [i,j] in Indices G & g /. n = G * (i,j) ) by A40, GOBOARD1:23;
A422: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_g2_&_n_+_1_in_dom_g2_holds_
for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g2_/._n_=_G_*_(l1,l2)_&_g2_/._(n_+_1)_=_G_*_(l3,l4)_holds_
(abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1
let n be Element of NAT ; ::_thesis: ( n in dom g2 & n + 1 in dom g2 implies for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds
(abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A423: n in dom g2 and
A424: n + 1 in dom g2 ; ::_thesis: for l1, l2, l3, l4 being Element of NAT st [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) holds
(abs (l1 - l3)) + (abs (l2 - l4)) = 1
let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g2 /. n = G * (l1,l2) & g2 /. (n + 1) = G * (l3,l4) implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A425: [l1,l2] in Indices G and
A426: [l3,l4] in Indices G and
A427: g2 /. n = G * (l1,l2) and
A428: g2 /. (n + 1) = G * (l3,l4) ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1
( g2 /. (n + 1) = G * ((i1 + (n + 1)),i2) & [(i1 + (n + 1)),i2] in Indices G ) by A413, A414, A419, A424;
then A429: ( l3 = i1 + (n + 1) & l4 = i2 ) by A426, A428, GOBOARD1:5;
( g2 /. n = G * ((i1 + n),i2) & [(i1 + n),i2] in Indices G ) by A413, A414, A419, A423;
then ( l1 = i1 + n & l2 = i2 ) by A425, A427, GOBOARD1:5;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs ((i1 + n) - (i1 + (n + 1)))) + 0 by A429, ABSVALUE:2
.= abs (- 1)
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
now__::_thesis:_for_l1,_l2,_l3,_l4_being_Element_of_NAT_st_[l1,l2]_in_Indices_G_&_[l3,l4]_in_Indices_G_&_g1_/._(len_g1)_=_G_*_(l1,l2)_&_g2_/._1_=_G_*_(l3,l4)_&_len_g1_in_dom_g1_&_1_in_dom_g2_holds_
(abs_(l1_-_l3))_+_(abs_(l2_-_l4))_=_1
let l1, l2, l3, l4 be Element of NAT ; ::_thesis: ( [l1,l2] in Indices G & [l3,l4] in Indices G & g1 /. (len g1) = G * (l1,l2) & g2 /. 1 = G * (l3,l4) & len g1 in dom g1 & 1 in dom g2 implies (abs (l1 - l3)) + (abs (l2 - l4)) = 1 )
assume that
A430: [l1,l2] in Indices G and
A431: [l3,l4] in Indices G and
A432: g1 /. (len g1) = G * (l1,l2) and
A433: g2 /. 1 = G * (l3,l4) and
len g1 in dom g1 and
A434: 1 in dom g2 ; ::_thesis: (abs (l1 - l3)) + (abs (l2 - l4)) = 1
( g2 /. 1 = G * ((i1 + 1),i2) & [(i1 + 1),i2] in Indices G ) by A413, A414, A419, A434;
then A435: ( l3 = i1 + 1 & l4 = i2 ) by A431, A433, GOBOARD1:5;
(f | k) /. (len (f | k)) = f /. k by A17, A23, A14, FINSEQ_4:71;
then ( l1 = i1 & l2 = i2 ) by A38, A18, A19, A430, A432, GOBOARD1:5;
hence (abs (l1 - l3)) + (abs (l2 - l4)) = (abs (i1 - (i1 + 1))) + 0 by A435, ABSVALUE:2
.= abs ((i1 - i1) + (- 1))
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def_1 ;
::_thesis: verum
end;
then for n being Element of NAT st n in dom g & n + 1 in dom g holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 by A41, A422, GOBOARD1:24;
hence g is_sequence_on G by A421, GOBOARD1:def_9; ::_thesis: ( L~ g = L~ f & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
A436: G * (j1,i2) = |[((G * (j1,i2)) `1),((G * (j1,i2)) `2)]| by EUCLID:53;
c1 /. j1 = c1 . j1 by A48, A43, PARTFUN1:def_6;
then A437: c1 /. j1 = G * (j1,i2) by A48, MATRIX_1:def_8;
then A438: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, GOBOARD1:def_1;
c1 /. i1 = c1 . i1 by A49, A43, PARTFUN1:def_6;
then A439: c1 /. i1 = G * (i1,i2) by A49, MATRIX_1:def_8;
then A440: (X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, GOBOARD1:def_1;
then A441: (G * (i1,i2)) `1 < (G * (j1,i2)) `1 by A49, A48, A52, A43, A22, A411, A438, SEQM_3:def_1;
A442: (Y_axis c1) . j1 = (G * (j1,i2)) `2 by A48, A43, A21, A437, GOBOARD1:def_2;
(Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A439, GOBOARD1:def_2;
then A443: (G * (i1,i2)) `2 = (G * (j1,i2)) `2 by A49, A48, A53, A43, A21, A442, SEQM_3:def_10;
A444: LSeg (f,k) = LSeg ((G * (i1,i2)),(G * (j1,i2))) by A3, A13, A19, A46, A294, TOPREAL1:def_3
.= { w where w is Point of (TOP-REAL 2) : ( w `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= w `1 & w `1 <= (G * (j1,i2)) `1 ) } by A441, A443, A412, A436, TOPREAL3:10 ;
A445: dom g2 = Seg l by A413, FINSEQ_1:def_3;
thus L~ g = L~ f ::_thesis: ( g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
proof
set lg = { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } ;
set lf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
A446: len g = (len g1) + (len g2) by FINSEQ_1:22;
A447: now__::_thesis:_for_j_being_Element_of_NAT_st_len_g1_<=_j_&_j_<=_len_g_holds_
for_p_being_Point_of_(TOP-REAL_2)_st_p_=_g_/._j_holds_
(_p_`2_=_(G_*_(i1,i2))_`2_&_(G_*_(i1,i2))_`1_<=_p_`1_&_p_`1_<=_(G_*_(j1,i2))_`1_&_p_in_rng_c1_)
let j be Element of NAT ; ::_thesis: ( len g1 <= j & j <= len g implies for p being Point of (TOP-REAL 2) st p = g /. j holds
( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) )
assume that
A448: len g1 <= j and
A449: j <= len g ; ::_thesis: for p being Point of (TOP-REAL 2) st p = g /. j holds
( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
reconsider w = j - (len g1) as Element of NAT by A448, INT_1:5;
set u = i1 + w;
let p be Point of (TOP-REAL 2); ::_thesis: ( p = g /. j implies ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) )
assume A450: p = g /. j ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
now__::_thesis:_(_p_`2_=_(G_*_(i1,i2))_`2_&_(G_*_(i1,i2))_`1_<=_p_`1_&_p_`1_<=_(G_*_(j1,i2))_`1_&_p_in_rng_c1_)
percases ( j = len g1 or j <> len g1 ) ;
supposeA451: j = len g1 ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then A452: g /. (len g1) = (f | k) /. (len (f | k)) by A38, FINSEQ_4:68
.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;
hence p `2 = (G * (i1,i2)) `2 by A450, A451; ::_thesis: ( (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
thus ( (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 ) by A49, A48, A52, A43, A22, A411, A440, A438, A450, A451, A452, SEQM_3:def_1; ::_thesis: p in rng c1
thus p in rng c1 by A49, A43, A439, A450, A451, A452, PARTFUN2:2; ::_thesis: verum
end;
supposeA453: j <> len g1 ; ::_thesis: ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
A454: w + (len g1) = j ;
then A455: w <= len g2 by A446, A449, XREAL_1:6;
A456: (Y_axis c1) . i1 = (G * (i1,i2)) `2 by A49, A43, A21, A439, GOBOARD1:def_2;
A457: j - (len g1) <> 0 by A453;
then A458: w >= 1 by NAT_1:14;
then A459: g /. j = g2 /. w by A454, A455, SEQ_4:136;
A460: i1 < i1 + w by A457, XREAL_1:29;
A461: w in dom g2 by A458, A455, FINSEQ_3:25;
then A462: i1 + w in dom G by A445, A414;
c1 /. (i1 + w) = c1 . (i1 + w) by A43, A445, A414, A461, PARTFUN1:def_6;
then A463: c1 /. (i1 + w) = G * ((i1 + w),i2) by A462, MATRIX_1:def_8;
then A464: (X_axis c1) . (i1 + w) = (G * ((i1 + w),i2)) `1 by A43, A22, A462, GOBOARD1:def_1;
A465: g2 /. w = G * ((i1 + w),i2) by A413, A461;
(Y_axis c1) . (i1 + w) = (G * ((i1 + w),i2)) `2 by A43, A21, A462, A463, GOBOARD1:def_2;
hence p `2 = (G * (i1,i2)) `2 by A49, A53, A43, A21, A450, A459, A465, A462, A456, SEQM_3:def_10; ::_thesis: ( (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
(X_axis c1) . i1 = (G * (i1,i2)) `1 by A49, A43, A22, A439, GOBOARD1:def_1;
hence (G * (i1,i2)) `1 <= p `1 by A49, A52, A43, A22, A450, A459, A465, A462, A464, A460, SEQM_3:def_1; ::_thesis: ( p `1 <= (G * (j1,i2)) `1 & p in rng c1 )
A466: (X_axis c1) . j1 = (G * (j1,i2)) `1 by A48, A43, A22, A437, GOBOARD1:def_1;
now__::_thesis:_p_`1_<=_(G_*_(j1,i2))_`1
percases ( i1 + w = j1 or i1 + w <> j1 ) ;
suppose i1 + w = j1 ; ::_thesis: p `1 <= (G * (j1,i2)) `1
hence p `1 <= (G * (j1,i2)) `1 by A450, A458, A454, A455, A465, SEQ_4:136; ::_thesis: verum
end;
supposeA467: i1 + w <> j1 ; ::_thesis: p `1 <= (G * (j1,i2)) `1
i1 + w <= i1 + l by A413, A455, XREAL_1:7;
then i1 + w < j1 by A467, XXREAL_0:1;
hence p `1 <= (G * (j1,i2)) `1 by A48, A52, A43, A22, A450, A459, A465, A462, A464, A466, SEQM_3:def_1; ::_thesis: verum
end;
end;
end;
hence p `1 <= (G * (j1,i2)) `1 ; ::_thesis: p in rng c1
thus p in rng c1 by A43, A450, A459, A465, A462, A463, PARTFUN2:2; ::_thesis: verum
end;
end;
end;
hence ( p `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= p `1 & p `1 <= (G * (j1,i2)) `1 & p in rng c1 ) ; ::_thesis: verum
end;
thus L~ g c= L~ f :: according to XBOOLE_0:def_10 ::_thesis: L~ f c= L~ g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ g or x in L~ f )
assume x in L~ g ; ::_thesis: x in L~ f
then consider X being set such that
A468: x in X and
A469: X in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by TARSKI:def_4;
consider i being Element of NAT such that
A470: X = LSeg (g,i) and
A471: 1 <= i and
A472: i + 1 <= len g by A469;
now__::_thesis:_x_in_L~_f
percases ( i + 1 <= len g1 or i + 1 > len g1 ) ;
supposeA473: i + 1 <= len g1 ; ::_thesis: x in L~ f
i <= i + 1 by NAT_1:11;
then i <= len g1 by A473, XXREAL_0:2;
then A474: i in dom g1 by A471, FINSEQ_3:25;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom g1 by A473, FINSEQ_3:25;
then X = LSeg (g1,i) by A470, A474, TOPREAL3:18;
then X in { (LSeg (g1,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g1 ) } by A471, A473;
then A475: x in L~ (f | k) by A36, A468, TARSKI:def_4;
L~ (f | k) c= L~ f by TOPREAL3:20;
hence x in L~ f by A475; ::_thesis: verum
end;
supposeA476: i + 1 > len g1 ; ::_thesis: x in L~ f
reconsider q1 = g /. i, q2 = g /. (i + 1) as Point of (TOP-REAL 2) ;
A477: i <= len g by A472, NAT_1:13;
A478: len g1 <= i by A476, NAT_1:13;
then A479: q1 `2 = (G * (i1,i2)) `2 by A447, A477;
A480: q1 `1 <= (G * (j1,i2)) `1 by A447, A478, A477;
A481: (G * (i1,i2)) `1 <= q1 `1 by A447, A478, A477;
q2 `2 = (G * (i1,i2)) `2 by A447, A472, A476;
then A482: q2 = |[(q2 `1),(q1 `2)]| by A479, EUCLID:53;
A483: q2 `1 <= (G * (j1,i2)) `1 by A447, A472, A476;
A484: ( q1 = |[(q1 `1),(q1 `2)]| & LSeg (g,i) = LSeg (q2,q1) ) by A471, A472, EUCLID:53, TOPREAL1:def_3;
A485: (G * (i1,i2)) `1 <= q2 `1 by A447, A472, A476;
now__::_thesis:_x_in_L~_f
percases ( q1 `1 > q2 `1 or q1 `1 = q2 `1 or q1 `1 < q2 `1 ) by XXREAL_0:1;
suppose q1 `1 > q2 `1 ; ::_thesis: x in L~ f
then LSeg (g,i) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q1 `2 & q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) } by A482, A484, TOPREAL3:10;
then consider p2 being Point of (TOP-REAL 2) such that
A486: ( p2 = x & p2 `2 = q1 `2 ) and
A487: ( q2 `1 <= p2 `1 & p2 `1 <= q1 `1 ) by A468, A470;
( (G * (i1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (j1,i2)) `1 ) by A480, A485, A487, XXREAL_0:2;
then A488: x in LSeg (f,k) by A444, A479, A486;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A488, TARSKI:def_4; ::_thesis: verum
end;
suppose q1 `1 = q2 `1 ; ::_thesis: x in L~ f
then LSeg (g,i) = {q1} by A482, A484, RLTOPSP1:70;
then x = q1 by A468, A470, TARSKI:def_1;
then A489: x in LSeg (f,k) by A444, A479, A481, A480;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A489, TARSKI:def_4; ::_thesis: verum
end;
suppose q1 `1 < q2 `1 ; ::_thesis: x in L~ f
then LSeg (g,i) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = q1 `2 & q1 `1 <= p1 `1 & p1 `1 <= q2 `1 ) } by A482, A484, TOPREAL3:10;
then consider p2 being Point of (TOP-REAL 2) such that
A490: ( p2 = x & p2 `2 = q1 `2 ) and
A491: ( q1 `1 <= p2 `1 & p2 `1 <= q2 `1 ) by A468, A470;
( (G * (i1,i2)) `1 <= p2 `1 & p2 `1 <= (G * (j1,i2)) `1 ) by A481, A483, A491, XXREAL_0:2;
then A492: x in LSeg (f,k) by A444, A479, A490;
LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A3, A13;
hence x in L~ f by A492, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in L~ f ; ::_thesis: verum
end;
end;
end;
hence x in L~ f ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ f or x in L~ g )
assume x in L~ f ; ::_thesis: x in L~ g
then A493: x in (L~ (f | k)) \/ (LSeg (f,k)) by A3, A12, Th3;
now__::_thesis:_x_in_L~_g
percases ( x in L~ (f | k) or x in LSeg (f,k) ) by A493, XBOOLE_0:def_3;
supposeA494: x in L~ (f | k) ; ::_thesis: x in L~ g
L~ g1 c= L~ g by Th6;
hence x in L~ g by A36, A494; ::_thesis: verum
end;
suppose x in LSeg (f,k) ; ::_thesis: x in L~ g
then consider p1 being Point of (TOP-REAL 2) such that
A495: p1 = x and
A496: p1 `2 = (G * (i1,i2)) `2 and
A497: (G * (i1,i2)) `1 <= p1 `1 and
A498: p1 `1 <= (G * (j1,i2)) `1 by A444;
defpred S2[ Nat] means ( len g1 <= $1 & $1 <= len g & ( for q being Point of (TOP-REAL 2) st q = g /. $1 holds
q `1 <= p1 `1 ) );
A499: now__::_thesis:_ex_n_being_Nat_st_S2[n]
reconsider n = len g1 as Nat ;
take n = n; ::_thesis: S2[n]
thus S2[n] ::_thesis: verum
proof
thus ( len g1 <= n & n <= len g ) by A446, XREAL_1:31; ::_thesis: for q being Point of (TOP-REAL 2) st q = g /. n holds
q `1 <= p1 `1
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then A500: len g1 in dom g1 by FINSEQ_3:25;
let q be Point of (TOP-REAL 2); ::_thesis: ( q = g /. n implies q `1 <= p1 `1 )
assume q = g /. n ; ::_thesis: q `1 <= p1 `1
then q = (f | k) /. (len (f | k)) by A38, A500, FINSEQ_4:68
.= G * (i1,i2) by A17, A23, A14, A19, FINSEQ_4:71 ;
hence q `1 <= p1 `1 by A497; ::_thesis: verum
end;
end;
A501: for n being Nat st S2[n] holds
n <= len g ;
consider ma being Nat such that
A502: ( S2[ma] & ( for n being Nat st S2[n] holds
n <= ma ) ) from NAT_1:sch_6(A501, A499);
reconsider ma = ma as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_x_in_L~_g
percases ( ma = len g or ma <> len g ) ;
supposeA503: ma = len g ; ::_thesis: x in L~ g
i1 + 1 <= j1 by A411, NAT_1:13;
then A504: 1 <= l by XREAL_1:19;
then 0 + 1 <= ma by A413, A446, A503, XREAL_1:7;
then reconsider m1 = ma - 1 as Element of NAT by INT_1:5;
A505: m1 + 1 = ma ;
(len g1) + 1 <= ma by A413, A446, A503, A504, XREAL_1:7;
then A506: m1 >= len g1 by A505, XREAL_1:6;
reconsider q = g /. m1 as Point of (TOP-REAL 2) ;
set lq = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & q `1 <= e `1 & e `1 <= (G * (j1,i2)) `1 ) } ;
A507: i1 + l = j1 ;
A508: l in dom g2 by A413, A504, FINSEQ_3:25;
then A509: g /. ma = g2 /. l by A413, A446, A503, FINSEQ_4:69
.= G * (j1,i2) by A413, A508, A507 ;
then (G * (j1,i2)) `1 <= p1 `1 by A502;
then A510: p1 `1 = (G * (j1,i2)) `1 by A498, XXREAL_0:1;
A511: m1 <= len g by A503, A505, NAT_1:11;
then A512: q `2 = (G * (i1,i2)) `2 by A447, A506;
A513: q `1 <= (G * (j1,i2)) `1 by A447, A506, A511;
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then A514: 1 <= m1 by A506, XXREAL_0:2;
then ( q = |[(q `1),(q `2)]| & LSeg (g,m1) = LSeg ((G * (j1,i2)),q) ) by A503, A509, A505, EUCLID:53, TOPREAL1:def_3;
then LSeg (g,m1) = { e where e is Point of (TOP-REAL 2) : ( e `2 = (G * (i1,i2)) `2 & q `1 <= e `1 & e `1 <= (G * (j1,i2)) `1 ) } by A443, A436, A512, A513, TOPREAL3:10;
then A515: p1 in LSeg (g,m1) by A496, A510, A513;
LSeg (g,m1) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A503, A505, A514;
hence x in L~ g by A495, A515, TARSKI:def_4; ::_thesis: verum
end;
suppose ma <> len g ; ::_thesis: x in L~ g
then ma < len g by A502, XXREAL_0:1;
then A516: ma + 1 <= len g by NAT_1:13;
reconsider qa = g /. ma, qa1 = g /. (ma + 1) as Point of (TOP-REAL 2) ;
set lma = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * (i1,i2)) `2 & qa `1 <= p2 `1 & p2 `1 <= qa1 `1 ) } ;
A517: qa1 = |[(qa1 `1),(qa1 `2)]| by EUCLID:53;
A518: qa `1 <= p1 `1 by A502;
A519: len g1 <= ma + 1 by A502, NAT_1:13;
then A520: qa1 `2 = (G * (i1,i2)) `2 by A447, A516;
A521: now__::_thesis:_not_qa1_`1_<=_p1_`1
assume qa1 `1 <= p1 `1 ; ::_thesis: contradiction
then for q being Point of (TOP-REAL 2) st q = g /. (ma + 1) holds
q `1 <= p1 `1 ;
then ma + 1 <= ma by A502, A516, A519;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
A522: ( qa `2 = (G * (i1,i2)) `2 & qa = |[(qa `1),(qa `2)]| ) by A447, A502, EUCLID:53;
A523: 1 <= ma by A13, A23, A39, A502, NAT_1:13;
then LSeg (g,ma) = LSeg (qa,qa1) by A516, TOPREAL1:def_3
.= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = (G * (i1,i2)) `2 & qa `1 <= p2 `1 & p2 `1 <= qa1 `1 ) } by A518, A521, A520, A522, A517, TOPREAL3:10, XXREAL_0:2 ;
then A524: x in LSeg (g,ma) by A495, A496, A518, A521;
LSeg (g,ma) in { (LSeg (g,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len g ) } by A523, A516;
hence x in L~ g by A524, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in L~ g ; ::_thesis: verum
end;
end;
end;
hence x in L~ g ; ::_thesis: verum
end;
1 <= len g1 by A13, A23, A39, XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:25;
hence g /. 1 = (f | k) /. 1 by A37, FINSEQ_4:68
.= f /. 1 by A17, A15, FINSEQ_4:71 ;
::_thesis: ( g /. (len g) = f /. (len f) & len f <= len g )
A525: len g = (len g1) + l by A413, FINSEQ_1:22;
i1 + 1 <= j1 by A411, NAT_1:13;
then A526: 1 <= l by XREAL_1:19;
then A527: l in dom g2 by A413, A419, FINSEQ_1:1;
hence g /. (len g) = g2 /. l by A525, FINSEQ_4:69
.= G * ((i1 + l),i2) by A413, A527
.= f /. (len f) by A3, A46, A294 ;
::_thesis: len f <= len g
thus len f <= len g by A3, A23, A39, A526, A525, XREAL_1:7; ::_thesis: verum
end;
end;
end;
hence ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; ::_thesis: verum
end;
end;
end;
hence ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; ::_thesis: verum
end;
end;
end;
hence ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ; ::_thesis: verum
end;
A528: S1[ 0 ]
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f = 0 & ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) )
assume that
A529: len f = 0 and
A530: for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) and
f is special and
for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ; ::_thesis: ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
take g = f; ::_thesis: ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
f = {} by A529;
then for n being Element of NAT st n in dom g & n + 1 in dom g holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & g /. n = G * (m,k) & g /. (n + 1) = G * (i,j) holds
(abs (m - i)) + (abs (k - j)) = 1 ;
hence ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) by A530, GOBOARD1:def_9; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A528, A1);
hence ( ( for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ) implies ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) ) ; ::_thesis: verum
end;
definition
let v1, v2 be FinSequence of REAL ;
assume A1: v1 <> {} ;
func GoB (v1,v2) -> Matrix of (TOP-REAL 2) means :Def1: :: GOBOARD2:def 1
( len it = len v1 & width it = len v2 & ( for n, m being Element of NAT st [n,m] in Indices it holds
it * (n,m) = |[(v1 . n),(v2 . m)]| ) );
existence
ex b1 being Matrix of (TOP-REAL 2) st
( len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds
b1 * (n,m) = |[(v1 . n),(v2 . m)]| ) )
proof
defpred S1[ Nat, Nat, Point of (TOP-REAL 2)] means ( [$1,$2] in [:(dom v1),(dom v2):] & ( for r, s being Real st v1 . $1 = r & v2 . $2 = s holds
$3 = |[r,s]| ) );
A2: dom v1 = Seg (len v1) by FINSEQ_1:def_3;
A3: for i, j being Nat st [i,j] in [:(Seg (len v1)),(Seg (len v2)):] holds
ex p being Point of (TOP-REAL 2) st S1[i,j,p]
proof
let i, j be Nat; ::_thesis: ( [i,j] in [:(Seg (len v1)),(Seg (len v2)):] implies ex p being Point of (TOP-REAL 2) st S1[i,j,p] )
assume A4: [i,j] in [:(Seg (len v1)),(Seg (len v2)):] ; ::_thesis: ex p being Point of (TOP-REAL 2) st S1[i,j,p]
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def_12;
reconsider s1 = v1 . i9, s2 = v2 . j9 as Real ;
take |[s1,s2]| ; ::_thesis: S1[i,j,|[s1,s2]|]
thus [i,j] in [:(dom v1),(dom v2):] by A2, A4, FINSEQ_1:def_3; ::_thesis: for r, s being Real st v1 . i = r & v2 . j = s holds
|[s1,s2]| = |[r,s]|
let r, s be Real; ::_thesis: ( v1 . i = r & v2 . j = s implies |[s1,s2]| = |[r,s]| )
assume ( r = v1 . i & s = v2 . j ) ; ::_thesis: |[s1,s2]| = |[r,s]|
hence |[s1,s2]| = |[r,s]| ; ::_thesis: verum
end;
consider M being Matrix of len v1, len v2, the carrier of (TOP-REAL 2) such that
A5: for i, j being Nat st [i,j] in Indices M holds
S1[i,j,M * (i,j)] from MATRIX_1:sch_2(A3);
reconsider M = M as Matrix of the carrier of (TOP-REAL 2) ;
take M ; ::_thesis: ( len M = len v1 & width M = len v2 & ( for n, m being Element of NAT st [n,m] in Indices M holds
M * (n,m) = |[(v1 . n),(v2 . m)]| ) )
thus ( len M = len v1 & width M = len v2 ) by A1, MATRIX_1:23; ::_thesis: for n, m being Element of NAT st [n,m] in Indices M holds
M * (n,m) = |[(v1 . n),(v2 . m)]|
let n, m be Element of NAT ; ::_thesis: ( [n,m] in Indices M implies M * (n,m) = |[(v1 . n),(v2 . m)]| )
assume [n,m] in Indices M ; ::_thesis: M * (n,m) = |[(v1 . n),(v2 . m)]|
hence M * (n,m) = |[(v1 . n),(v2 . m)]| by A5; ::_thesis: verum
end;
uniqueness
for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds
b1 * (n,m) = |[(v1 . n),(v2 . m)]| ) & len b2 = len v1 & width b2 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b2 holds
b2 * (n,m) = |[(v1 . n),(v2 . m)]| ) holds
b1 = b2
proof
let G1, G2 be Matrix of (TOP-REAL 2); ::_thesis: ( len G1 = len v1 & width G1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices G1 holds
G1 * (n,m) = |[(v1 . n),(v2 . m)]| ) & len G2 = len v1 & width G2 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices G2 holds
G2 * (n,m) = |[(v1 . n),(v2 . m)]| ) implies G1 = G2 )
assume that
A6: ( len G1 = len v1 & width G1 = len v2 ) and
A7: for n, m being Element of NAT st [n,m] in Indices G1 holds
G1 * (n,m) = |[(v1 . n),(v2 . m)]| and
A8: ( len G2 = len v1 & width G2 = len v2 ) and
A9: for n, m being Element of NAT st [n,m] in Indices G2 holds
G2 * (n,m) = |[(v1 . n),(v2 . m)]| ; ::_thesis: G1 = G2
A10: ( Indices G1 = [:(dom G1),(Seg (width G1)):] & Indices G2 = [:(dom G2),(Seg (width G2)):] ) by MATRIX_1:def_4;
now__::_thesis:_for_n,_m_being_Nat_st_[n,m]_in_Indices_G1_holds_
G1_*_(n,m)_=_G2_*_(n,m)
let n, m be Nat; ::_thesis: ( [n,m] in Indices G1 implies G1 * (n,m) = G2 * (n,m) )
reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def_12;
A11: ( dom G1 = Seg (len G1) & dom G2 = Seg (len G2) ) by FINSEQ_1:def_3;
reconsider r = v1 . n9, s = v2 . m9 as Real ;
assume A12: [n,m] in Indices G1 ; ::_thesis: G1 * (n,m) = G2 * (n,m)
then G1 * (n,m) = |[r,s]| by A7;
hence G1 * (n,m) = G2 * (n,m) by A6, A8, A9, A10, A12, A11; ::_thesis: verum
end;
hence G1 = G2 by A6, A8, MATRIX_1:21; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines GoB GOBOARD2:def_1_:_
for v1, v2 being FinSequence of REAL st v1 <> {} holds
for b3 being Matrix of (TOP-REAL 2) holds
( b3 = GoB (v1,v2) iff ( len b3 = len v1 & width b3 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b3 holds
b3 * (n,m) = |[(v1 . n),(v2 . m)]| ) ) );
registration
let v1, v2 be non empty FinSequence of REAL ;
cluster GoB (v1,v2) -> V3() X_equal-in-line Y_equal-in-column ;
coherence
( not GoB (v1,v2) is empty-yielding & GoB (v1,v2) is X_equal-in-line & GoB (v1,v2) is Y_equal-in-column )
proof
set M = GoB (v1,v2);
A1: len (GoB (v1,v2)) = len v1 by Def1;
then A2: dom (GoB (v1,v2)) = dom v1 by FINSEQ_3:29;
A3: width (GoB (v1,v2)) = len v2 by Def1;
hence GoB (v1,v2) is V3() by A1, GOBOARD1:def_3; ::_thesis: ( GoB (v1,v2) is X_equal-in-line & GoB (v1,v2) is Y_equal-in-column )
A4: Indices (GoB (v1,v2)) = [:(dom v1),(Seg (len v2)):] by A3, A2, MATRIX_1:def_4;
thus GoB (v1,v2) is X_equal-in-line ::_thesis: GoB (v1,v2) is Y_equal-in-column
proof
let n be Element of NAT ; :: according to GOBOARD1:def_4 ::_thesis: ( not n in dom (GoB (v1,v2)) or X_axis (Line ((GoB (v1,v2)),n)) is constant )
reconsider l = Line ((GoB (v1,v2)),n) as FinSequence of (TOP-REAL 2) ;
set x = X_axis l;
assume A5: n in dom (GoB (v1,v2)) ; ::_thesis: X_axis (Line ((GoB (v1,v2)),n)) is constant
A6: ( len l = width (GoB (v1,v2)) & dom (X_axis l) = Seg (len (X_axis l)) ) by FINSEQ_1:def_3, MATRIX_1:def_7;
A7: len (X_axis l) = len l by GOBOARD1:def_1;
then A8: dom (X_axis l) = dom l by FINSEQ_3:29;
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_(X_axis_l)_&_j_in_dom_(X_axis_l)_holds_
(X_axis_l)_._i_=_(X_axis_l)_._j
let i, j be Element of NAT ; ::_thesis: ( i in dom (X_axis l) & j in dom (X_axis l) implies (X_axis l) . i = (X_axis l) . j )
assume that
A9: i in dom (X_axis l) and
A10: j in dom (X_axis l) ; ::_thesis: (X_axis l) . i = (X_axis l) . j
reconsider r = v1 . n, s1 = v2 . i, s2 = v2 . j as Real ;
[n,i] in Indices (GoB (v1,v2)) by A3, A2, A4, A5, A7, A6, A9, ZFMISC_1:87;
then (GoB (v1,v2)) * (n,i) = |[r,s1]| by Def1;
then A11: ((GoB (v1,v2)) * (n,i)) `1 = r by EUCLID:52;
l /. i = l . i by A8, A9, PARTFUN1:def_6;
then l /. i = (GoB (v1,v2)) * (n,i) by A7, A6, A9, MATRIX_1:def_7;
then A12: (X_axis l) . i = r by A9, A11, GOBOARD1:def_1;
[n,j] in Indices (GoB (v1,v2)) by A3, A2, A4, A5, A7, A6, A10, ZFMISC_1:87;
then (GoB (v1,v2)) * (n,j) = |[r,s2]| by Def1;
then A13: ((GoB (v1,v2)) * (n,j)) `1 = r by EUCLID:52;
l /. j = l . j by A8, A10, PARTFUN1:def_6;
then l /. j = (GoB (v1,v2)) * (n,j) by A7, A6, A10, MATRIX_1:def_7;
hence (X_axis l) . i = (X_axis l) . j by A10, A13, A12, GOBOARD1:def_1; ::_thesis: verum
end;
hence X_axis (Line ((GoB (v1,v2)),n)) is constant by SEQM_3:def_10; ::_thesis: verum
end;
thus GoB (v1,v2) is Y_equal-in-column ::_thesis: verum
proof
let n be Element of NAT ; :: according to GOBOARD1:def_5 ::_thesis: ( not n in Seg (width (GoB (v1,v2))) or Y_axis (Col ((GoB (v1,v2)),n)) is constant )
reconsider c = Col ((GoB (v1,v2)),n) as FinSequence of (TOP-REAL 2) ;
set y = Y_axis c;
len (Y_axis c) = len c by GOBOARD1:def_2;
then A14: dom (Y_axis c) = dom c by FINSEQ_3:29;
len c = len (GoB (v1,v2)) by MATRIX_1:def_8;
then A15: dom c = dom (GoB (v1,v2)) by FINSEQ_3:29;
assume A16: n in Seg (width (GoB (v1,v2))) ; ::_thesis: Y_axis (Col ((GoB (v1,v2)),n)) is constant
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_(Y_axis_c)_&_j_in_dom_(Y_axis_c)_holds_
(Y_axis_c)_._i_=_(Y_axis_c)_._j
let i, j be Element of NAT ; ::_thesis: ( i in dom (Y_axis c) & j in dom (Y_axis c) implies (Y_axis c) . i = (Y_axis c) . j )
assume that
A17: i in dom (Y_axis c) and
A18: j in dom (Y_axis c) ; ::_thesis: (Y_axis c) . i = (Y_axis c) . j
reconsider r = v2 . n, s1 = v1 . i, s2 = v1 . j as Real ;
[i,n] in Indices (GoB (v1,v2)) by A3, A2, A4, A16, A14, A15, A17, ZFMISC_1:87;
then (GoB (v1,v2)) * (i,n) = |[s1,r]| by Def1;
then A19: ((GoB (v1,v2)) * (i,n)) `2 = r by EUCLID:52;
c /. i = c . i by A14, A17, PARTFUN1:def_6;
then c /. i = (GoB (v1,v2)) * (i,n) by A14, A15, A17, MATRIX_1:def_8;
then A20: (Y_axis c) . i = r by A17, A19, GOBOARD1:def_2;
[j,n] in Indices (GoB (v1,v2)) by A3, A2, A4, A16, A14, A15, A18, ZFMISC_1:87;
then (GoB (v1,v2)) * (j,n) = |[s2,r]| by Def1;
then A21: ((GoB (v1,v2)) * (j,n)) `2 = r by EUCLID:52;
c /. j = c . j by A14, A18, PARTFUN1:def_6;
then c /. j = (GoB (v1,v2)) * (j,n) by A14, A15, A18, MATRIX_1:def_8;
hence (Y_axis c) . i = (Y_axis c) . j by A18, A21, A20, GOBOARD1:def_2; ::_thesis: verum
end;
hence Y_axis (Col ((GoB (v1,v2)),n)) is constant by SEQM_3:def_10; ::_thesis: verum
end;
end;
end;
registration
let v1, v2 be non empty increasing FinSequence of REAL ;
cluster GoB (v1,v2) -> Y_increasing-in-line X_increasing-in-column ;
coherence
( GoB (v1,v2) is Y_increasing-in-line & GoB (v1,v2) is X_increasing-in-column )
proof
set M = GoB (v1,v2);
A1: width (GoB (v1,v2)) = len v2 by Def1;
A2: len (GoB (v1,v2)) = len v1 by Def1;
then A3: dom (GoB (v1,v2)) = dom v1 by FINSEQ_3:29;
then A4: Indices (GoB (v1,v2)) = [:(dom v1),(Seg (len v2)):] by A1, MATRIX_1:def_4;
A5: dom v2 = Seg (len v2) by FINSEQ_1:def_3;
thus GoB (v1,v2) is Y_increasing-in-line ::_thesis: GoB (v1,v2) is X_increasing-in-column
proof
let n be Element of NAT ; :: according to GOBOARD1:def_6 ::_thesis: ( not n in dom (GoB (v1,v2)) or Y_axis (Line ((GoB (v1,v2)),n)) is increasing )
reconsider l = Line ((GoB (v1,v2)),n) as FinSequence of (TOP-REAL 2) ;
set y = Y_axis l;
assume A6: n in dom (GoB (v1,v2)) ; ::_thesis: Y_axis (Line ((GoB (v1,v2)),n)) is increasing
A7: ( len l = width (GoB (v1,v2)) & dom (Y_axis l) = Seg (len (Y_axis l)) ) by FINSEQ_1:def_3, MATRIX_1:def_7;
A8: len (Y_axis l) = len l by GOBOARD1:def_2;
then A9: dom (Y_axis l) = dom l by FINSEQ_3:29;
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_(Y_axis_l)_&_j_in_dom_(Y_axis_l)_&_i_<_j_holds_
(Y_axis_l)_._i_<_(Y_axis_l)_._j
let i, j be Element of NAT ; ::_thesis: ( i in dom (Y_axis l) & j in dom (Y_axis l) & i < j implies (Y_axis l) . i < (Y_axis l) . j )
assume that
A10: i in dom (Y_axis l) and
A11: j in dom (Y_axis l) and
A12: i < j ; ::_thesis: (Y_axis l) . i < (Y_axis l) . j
reconsider r = v1 . n, s1 = v2 . i, s2 = v2 . j as Real ;
[n,j] in Indices (GoB (v1,v2)) by A1, A3, A4, A6, A8, A7, A11, ZFMISC_1:87;
then (GoB (v1,v2)) * (n,j) = |[r,s2]| by Def1;
then A13: ((GoB (v1,v2)) * (n,j)) `2 = s2 by EUCLID:52;
l /. j = l . j by A9, A11, PARTFUN1:def_6;
then l /. j = (GoB (v1,v2)) * (n,j) by A8, A7, A11, MATRIX_1:def_7;
then A14: (Y_axis l) . j = s2 by A11, A13, GOBOARD1:def_2;
[n,i] in Indices (GoB (v1,v2)) by A1, A3, A4, A6, A8, A7, A10, ZFMISC_1:87;
then (GoB (v1,v2)) * (n,i) = |[r,s1]| by Def1;
then A15: ((GoB (v1,v2)) * (n,i)) `2 = s1 by EUCLID:52;
l /. i = l . i by A9, A10, PARTFUN1:def_6;
then l /. i = (GoB (v1,v2)) * (n,i) by A8, A7, A10, MATRIX_1:def_7;
then (Y_axis l) . i = s1 by A10, A15, GOBOARD1:def_2;
hence (Y_axis l) . i < (Y_axis l) . j by A5, A1, A8, A7, A10, A11, A12, A14, SEQM_3:def_1; ::_thesis: verum
end;
hence Y_axis (Line ((GoB (v1,v2)),n)) is increasing by SEQM_3:def_1; ::_thesis: verum
end;
A16: dom v1 = Seg (len v1) by FINSEQ_1:def_3;
thus GoB (v1,v2) is X_increasing-in-column ::_thesis: verum
proof
let n be Element of NAT ; :: according to GOBOARD1:def_7 ::_thesis: ( not n in Seg (width (GoB (v1,v2))) or X_axis (Col ((GoB (v1,v2)),n)) is increasing )
reconsider c = Col ((GoB (v1,v2)),n) as FinSequence of (TOP-REAL 2) ;
set x = X_axis c;
assume A17: n in Seg (width (GoB (v1,v2))) ; ::_thesis: X_axis (Col ((GoB (v1,v2)),n)) is increasing
A18: len (X_axis c) = len c by GOBOARD1:def_1;
then A19: dom (X_axis c) = dom c by FINSEQ_3:29;
A20: len c = len (GoB (v1,v2)) by MATRIX_1:def_8;
then A21: dom c = dom (GoB (v1,v2)) by FINSEQ_3:29;
A22: dom (X_axis c) = Seg (len (X_axis c)) by FINSEQ_1:def_3;
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_(X_axis_c)_&_j_in_dom_(X_axis_c)_&_i_<_j_holds_
(X_axis_c)_._i_<_(X_axis_c)_._j
let i, j be Element of NAT ; ::_thesis: ( i in dom (X_axis c) & j in dom (X_axis c) & i < j implies (X_axis c) . i < (X_axis c) . j )
assume that
A23: i in dom (X_axis c) and
A24: j in dom (X_axis c) and
A25: i < j ; ::_thesis: (X_axis c) . i < (X_axis c) . j
reconsider r = v2 . n, s1 = v1 . i, s2 = v1 . j as Real ;
[j,n] in Indices (GoB (v1,v2)) by A1, A3, A4, A17, A19, A21, A24, ZFMISC_1:87;
then (GoB (v1,v2)) * (j,n) = |[s2,r]| by Def1;
then A26: ((GoB (v1,v2)) * (j,n)) `1 = s2 by EUCLID:52;
c /. j = c . j by A19, A24, PARTFUN1:def_6;
then c /. j = (GoB (v1,v2)) * (j,n) by A19, A21, A24, MATRIX_1:def_8;
then A27: (X_axis c) . j = s2 by A24, A26, GOBOARD1:def_1;
[i,n] in Indices (GoB (v1,v2)) by A1, A3, A4, A17, A19, A21, A23, ZFMISC_1:87;
then (GoB (v1,v2)) * (i,n) = |[s1,r]| by Def1;
then A28: ((GoB (v1,v2)) * (i,n)) `1 = s1 by EUCLID:52;
c /. i = c . i by A19, A23, PARTFUN1:def_6;
then c /. i = (GoB (v1,v2)) * (i,n) by A19, A21, A23, MATRIX_1:def_8;
then (X_axis c) . i = s1 by A23, A28, GOBOARD1:def_1;
hence (X_axis c) . i < (X_axis c) . j by A16, A2, A18, A20, A22, A23, A24, A25, A27, SEQM_3:def_1; ::_thesis: verum
end;
hence X_axis (Col ((GoB (v1,v2)),n)) is increasing by SEQM_3:def_1; ::_thesis: verum
end;
end;
end;
definition
let f be non empty FinSequence of (TOP-REAL 2);
func GoB f -> Matrix of (TOP-REAL 2) equals :: GOBOARD2:def 2
GoB ((Incr (X_axis f)),(Incr (Y_axis f)));
correctness
coherence
GoB ((Incr (X_axis f)),(Incr (Y_axis f))) is Matrix of (TOP-REAL 2);
;
end;
:: deftheorem defines GoB GOBOARD2:def_2_:_
for f being non empty FinSequence of (TOP-REAL 2) holds GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f)));
registration
let f be non empty FinSequence of (TOP-REAL 2);
cluster GoB f -> V3() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ;
coherence
( not GoB f is empty-yielding & GoB f is X_equal-in-line & GoB f is Y_equal-in-column & GoB f is Y_increasing-in-line & GoB f is X_increasing-in-column ) ;
end;
theorem Th13: :: GOBOARD2:13
for f being non empty FinSequence of (TOP-REAL 2) holds
( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) )
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) )
set x = X_axis f;
set y = Y_axis f;
( len (Incr (X_axis f)) = card (rng (X_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by SEQ_4:def_21;
hence ( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) ) by Def1; ::_thesis: verum
end;
theorem :: GOBOARD2:14
for f being non empty FinSequence of (TOP-REAL 2)
for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
set x = X_axis f;
set y = Y_axis f;
let n be Element of NAT ; ::_thesis: ( n in dom f implies ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) )
assume A1: n in dom f ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
A2: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def_21;
reconsider p = f /. n as Point of (TOP-REAL 2) ;
A3: dom f = Seg (len f) by FINSEQ_1:def_3;
( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2;
then ( (Y_axis f) . n = p `2 & (Y_axis f) . n in rng (Y_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_2;
then consider j being Nat such that
A4: j in dom (Incr (Y_axis f)) and
A5: (Incr (Y_axis f)) . j = p `2 by A2, FINSEQ_2:10;
A6: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def_21;
( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1;
then ( (X_axis f) . n = p `1 & (X_axis f) . n in rng (X_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_1;
then consider i being Nat such that
A7: i in dom (Incr (X_axis f)) and
A8: (Incr (X_axis f)) . i = p `1 by A6, FINSEQ_2:10;
( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def_21;
then A9: Seg (width (GoB f)) = dom (Incr (Y_axis f)) by FINSEQ_1:def_3;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def_12;
take i ; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
take j ; ::_thesis: ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )
( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def_21;
then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (GoB f) = dom (Incr (X_axis f)) ) by FINSEQ_3:29, MATRIX_1:def_4;
hence [i,j] in Indices (GoB f) by A7, A4, A9, ZFMISC_1:87; ::_thesis: f /. n = (GoB f) * (i,j)
then (GoB f) * (i,j) = |[(p `1),(p `2)]| by A8, A5, Def1;
hence f /. n = (GoB f) * (i,j) by EUCLID:53; ::_thesis: verum
end;
theorem :: GOBOARD2:15
for n being Element of NAT
for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds
(X_axis f) . n <= (X_axis f) . m ) holds
f /. n in rng (Line ((GoB f),1))
proof
let n be Element of NAT ; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds
(X_axis f) . n <= (X_axis f) . m ) holds
f /. n in rng (Line ((GoB f),1))
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( n in dom f & ( for m being Element of NAT st m in dom f holds
(X_axis f) . n <= (X_axis f) . m ) implies f /. n in rng (Line ((GoB f),1)) )
set x = X_axis f;
set y = Y_axis f;
set r = (X_axis f) . n;
assume that
A1: n in dom f and
A2: for m being Element of NAT st m in dom f holds
(X_axis f) . n <= (X_axis f) . m ; ::_thesis: f /. n in rng (Line ((GoB f),1))
reconsider p = f /. n as Point of (TOP-REAL 2) ;
A3: dom f = Seg (len f) by FINSEQ_1:def_3;
A4: ( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1;
then A5: (X_axis f) . n = p `1 by A1, A3, GOBOARD1:def_1;
A6: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def_21;
(X_axis f) . n in rng (X_axis f) by A1, A3, A4, FUNCT_1:def_3;
then consider i being Nat such that
A7: i in dom (Incr (X_axis f)) and
A8: (Incr (X_axis f)) . i = p `1 by A5, A6, FINSEQ_2:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
A9: 1 <= i by A7, FINSEQ_3:25;
then reconsider i1 = i - 1 as Element of NAT by INT_1:5;
A10: i <= len (Incr (X_axis f)) by A7, FINSEQ_3:25;
A11: now__::_thesis:_not_i_<>_1
reconsider s = (Incr (X_axis f)) . i1 as Real ;
assume i <> 1 ; ::_thesis: contradiction
then 1 < i by A9, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A12: 1 <= i1 by XREAL_1:19;
i1 <= i by XREAL_1:44;
then i1 <= len (Incr (X_axis f)) by A10, XXREAL_0:2;
then A13: i1 in dom (Incr (X_axis f)) by A12, FINSEQ_3:25;
then (Incr (X_axis f)) . i1 in rng (Incr (X_axis f)) by FUNCT_1:def_3;
then A14: ex m being Nat st
( m in dom (X_axis f) & (X_axis f) . m = s ) by A6, FINSEQ_2:10;
i1 < i by XREAL_1:44;
then s < (X_axis f) . n by A5, A7, A8, A13, SEQM_3:def_1;
hence contradiction by A2, A3, A4, A14; ::_thesis: verum
end;
A15: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def_21;
( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2;
then ( (Y_axis f) . n = p `2 & (Y_axis f) . n in rng (Y_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_2;
then consider j being Nat such that
A16: j in dom (Incr (Y_axis f)) and
A17: (Incr (Y_axis f)) . j = p `2 by A15, FINSEQ_2:10;
A18: p = |[(p `1),(p `2)]| by EUCLID:53;
len (Line ((GoB f),1)) = width (GoB f) by MATRIX_1:def_7;
then A19: dom (Line ((GoB f),1)) = Seg (width (GoB f)) by FINSEQ_1:def_3;
( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def_21;
then A20: dom (Incr (Y_axis f)) = Seg (width (GoB f)) by FINSEQ_1:def_3;
( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def_21;
then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (X_axis f)) = dom (GoB f) ) by FINSEQ_3:29, MATRIX_1:def_4;
then [1,j] in Indices (GoB f) by A7, A16, A20, A11, ZFMISC_1:87;
then (GoB f) * (1,j) = |[(p `1),(p `2)]| by A8, A16, A17, A11, Def1;
then (Line ((GoB f),1)) . j = f /. n by A16, A20, A18, MATRIX_1:def_7;
hence f /. n in rng (Line ((GoB f),1)) by A16, A20, A19, FUNCT_1:def_3; ::_thesis: verum
end;
theorem :: GOBOARD2:16
for n being Element of NAT
for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds
(X_axis f) . m <= (X_axis f) . n ) holds
f /. n in rng (Line ((GoB f),(len (GoB f))))
proof
let n be Element of NAT ; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds
(X_axis f) . m <= (X_axis f) . n ) holds
f /. n in rng (Line ((GoB f),(len (GoB f))))
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( n in dom f & ( for m being Element of NAT st m in dom f holds
(X_axis f) . m <= (X_axis f) . n ) implies f /. n in rng (Line ((GoB f),(len (GoB f)))) )
set x = X_axis f;
set y = Y_axis f;
set r = (X_axis f) . n;
assume that
A1: n in dom f and
A2: for m being Element of NAT st m in dom f holds
(X_axis f) . m <= (X_axis f) . n ; ::_thesis: f /. n in rng (Line ((GoB f),(len (GoB f))))
reconsider p = f /. n as Point of (TOP-REAL 2) ;
A3: dom f = Seg (len f) by FINSEQ_1:def_3;
A4: ( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1;
then A5: (X_axis f) . n = p `1 by A1, A3, GOBOARD1:def_1;
A6: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def_21;
(X_axis f) . n in rng (X_axis f) by A1, A3, A4, FUNCT_1:def_3;
then consider i being Nat such that
A7: i in dom (Incr (X_axis f)) and
A8: (Incr (X_axis f)) . i = p `1 by A5, A6, FINSEQ_2:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
A9: i <= len (Incr (X_axis f)) by A7, FINSEQ_3:25;
A10: 1 <= i by A7, FINSEQ_3:25;
A11: now__::_thesis:_not_i_<>_len_(Incr_(X_axis_f))
reconsider s = (Incr (X_axis f)) . (i + 1) as Real ;
assume i <> len (Incr (X_axis f)) ; ::_thesis: contradiction
then i < len (Incr (X_axis f)) by A9, XXREAL_0:1;
then A12: i + 1 <= len (Incr (X_axis f)) by NAT_1:13;
1 <= i + 1 by A10, NAT_1:13;
then A13: i + 1 in dom (Incr (X_axis f)) by A12, FINSEQ_3:25;
then (Incr (X_axis f)) . (i + 1) in rng (Incr (X_axis f)) by FUNCT_1:def_3;
then A14: ex m being Nat st
( m in dom (X_axis f) & (X_axis f) . m = s ) by A6, FINSEQ_2:10;
i < i + 1 by NAT_1:13;
then (X_axis f) . n < s by A5, A7, A8, A13, SEQM_3:def_1;
hence contradiction by A2, A3, A4, A14; ::_thesis: verum
end;
A15: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def_21;
( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2;
then ( (Y_axis f) . n = p `2 & (Y_axis f) . n in rng (Y_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_2;
then consider j being Nat such that
A16: j in dom (Incr (Y_axis f)) and
A17: (Incr (Y_axis f)) . j = p `2 by A15, FINSEQ_2:10;
A18: p = |[(p `1),(p `2)]| by EUCLID:53;
len (Line ((GoB f),(len (GoB f)))) = width (GoB f) by MATRIX_1:def_7;
then A19: dom (Line ((GoB f),(len (GoB f)))) = Seg (width (GoB f)) by FINSEQ_1:def_3;
( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def_21;
then A20: dom (Incr (Y_axis f)) = Seg (width (GoB f)) by FINSEQ_1:def_3;
A21: ( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def_21;
then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (X_axis f)) = dom (GoB f) ) by FINSEQ_3:29, MATRIX_1:def_4;
then [(len (GoB f)),j] in Indices (GoB f) by A21, A7, A16, A20, A11, ZFMISC_1:87;
then (GoB f) * ((len (GoB f)),j) = |[(p `1),(p `2)]| by A21, A8, A16, A17, A11, Def1;
then (Line ((GoB f),(len (GoB f)))) . j = f /. n by A16, A20, A18, MATRIX_1:def_7;
hence f /. n in rng (Line ((GoB f),(len (GoB f)))) by A16, A20, A19, FUNCT_1:def_3; ::_thesis: verum
end;
theorem :: GOBOARD2:17
for n being Element of NAT
for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds
(Y_axis f) . n <= (Y_axis f) . m ) holds
f /. n in rng (Col ((GoB f),1))
proof
let n be Element of NAT ; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds
(Y_axis f) . n <= (Y_axis f) . m ) holds
f /. n in rng (Col ((GoB f),1))
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( n in dom f & ( for m being Element of NAT st m in dom f holds
(Y_axis f) . n <= (Y_axis f) . m ) implies f /. n in rng (Col ((GoB f),1)) )
set x = X_axis f;
set y = Y_axis f;
set r = (Y_axis f) . n;
assume that
A1: n in dom f and
A2: for m being Element of NAT st m in dom f holds
(Y_axis f) . n <= (Y_axis f) . m ; ::_thesis: f /. n in rng (Col ((GoB f),1))
reconsider p = f /. n as Point of (TOP-REAL 2) ;
A3: dom f = Seg (len f) by FINSEQ_1:def_3;
A4: ( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2;
then A5: (Y_axis f) . n = p `2 by A1, A3, GOBOARD1:def_2;
A6: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def_21;
(Y_axis f) . n in rng (Y_axis f) by A1, A3, A4, FUNCT_1:def_3;
then consider j being Nat such that
A7: j in dom (Incr (Y_axis f)) and
A8: (Incr (Y_axis f)) . j = p `2 by A5, A6, FINSEQ_2:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A9: 1 <= j by A7, FINSEQ_3:25;
then reconsider j1 = j - 1 as Element of NAT by INT_1:5;
A10: j <= len (Incr (Y_axis f)) by A7, FINSEQ_3:25;
A11: now__::_thesis:_not_j_<>_1
reconsider s = (Incr (Y_axis f)) . j1 as Real ;
assume j <> 1 ; ::_thesis: contradiction
then 1 < j by A9, XXREAL_0:1;
then 1 + 1 <= j by NAT_1:13;
then A12: 1 <= j1 by XREAL_1:19;
j1 <= j by XREAL_1:44;
then j1 <= len (Incr (Y_axis f)) by A10, XXREAL_0:2;
then A13: j1 in dom (Incr (Y_axis f)) by A12, FINSEQ_3:25;
then (Incr (Y_axis f)) . j1 in rng (Incr (Y_axis f)) by FUNCT_1:def_3;
then A14: ex m being Nat st
( m in dom (Y_axis f) & (Y_axis f) . m = s ) by A6, FINSEQ_2:10;
j1 < j by XREAL_1:44;
then s < (Y_axis f) . n by A5, A7, A8, A13, SEQM_3:def_1;
hence contradiction by A2, A3, A4, A14; ::_thesis: verum
end;
A15: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def_21;
( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1;
then ( (X_axis f) . n = p `1 & (X_axis f) . n in rng (X_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_1;
then consider i being Nat such that
A16: i in dom (Incr (X_axis f)) and
A17: (Incr (X_axis f)) . i = p `1 by A15, FINSEQ_2:10;
A18: p = |[(p `1),(p `2)]| by EUCLID:53;
len (Col ((GoB f),1)) = len (GoB f) by MATRIX_1:def_8;
then A19: dom (Col ((GoB f),1)) = dom (GoB f) by FINSEQ_3:29;
( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def_21;
then A20: dom (Incr (X_axis f)) = dom (GoB f) by FINSEQ_3:29;
( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def_21;
then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (Y_axis f)) = Seg (width (GoB f)) ) by FINSEQ_1:def_3, MATRIX_1:def_4;
then [i,1] in Indices (GoB f) by A16, A7, A20, A11, ZFMISC_1:87;
then (GoB f) * (i,1) = |[(p `1),(p `2)]| by A16, A17, A8, A11, Def1;
then (Col ((GoB f),1)) . i = f /. n by A16, A20, A18, MATRIX_1:def_8;
hence f /. n in rng (Col ((GoB f),1)) by A16, A20, A19, FUNCT_1:def_3; ::_thesis: verum
end;
theorem :: GOBOARD2:18
for n being Element of NAT
for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds
(Y_axis f) . m <= (Y_axis f) . n ) holds
f /. n in rng (Col ((GoB f),(width (GoB f))))
proof
let n be Element of NAT ; ::_thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds
(Y_axis f) . m <= (Y_axis f) . n ) holds
f /. n in rng (Col ((GoB f),(width (GoB f))))
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( n in dom f & ( for m being Element of NAT st m in dom f holds
(Y_axis f) . m <= (Y_axis f) . n ) implies f /. n in rng (Col ((GoB f),(width (GoB f)))) )
set x = X_axis f;
set y = Y_axis f;
set r = (Y_axis f) . n;
assume that
A1: n in dom f and
A2: for m being Element of NAT st m in dom f holds
(Y_axis f) . m <= (Y_axis f) . n ; ::_thesis: f /. n in rng (Col ((GoB f),(width (GoB f))))
reconsider p = f /. n as Point of (TOP-REAL 2) ;
A3: dom f = Seg (len f) by FINSEQ_1:def_3;
A4: ( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_2;
then A5: (Y_axis f) . n = p `2 by A1, A3, GOBOARD1:def_2;
A6: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def_21;
(Y_axis f) . n in rng (Y_axis f) by A1, A3, A4, FUNCT_1:def_3;
then consider j being Nat such that
A7: j in dom (Incr (Y_axis f)) and
A8: (Incr (Y_axis f)) . j = p `2 by A5, A6, FINSEQ_2:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A9: j <= len (Incr (Y_axis f)) by A7, FINSEQ_3:25;
A10: 1 <= j by A7, FINSEQ_3:25;
A11: now__::_thesis:_not_j_<>_len_(Incr_(Y_axis_f))
reconsider s = (Incr (Y_axis f)) . (j + 1) as Real ;
assume j <> len (Incr (Y_axis f)) ; ::_thesis: contradiction
then j < len (Incr (Y_axis f)) by A9, XXREAL_0:1;
then A12: j + 1 <= len (Incr (Y_axis f)) by NAT_1:13;
1 <= j + 1 by A10, NAT_1:13;
then A13: j + 1 in dom (Incr (Y_axis f)) by A12, FINSEQ_3:25;
then (Incr (Y_axis f)) . (j + 1) in rng (Incr (Y_axis f)) by FUNCT_1:def_3;
then A14: ex m being Nat st
( m in dom (Y_axis f) & (Y_axis f) . m = s ) by A6, FINSEQ_2:10;
j < j + 1 by NAT_1:13;
then (Y_axis f) . n < s by A5, A7, A8, A13, SEQM_3:def_1;
hence contradiction by A2, A3, A4, A14; ::_thesis: verum
end;
A15: rng (Incr (X_axis f)) = rng (X_axis f) by SEQ_4:def_21;
( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def_3, GOBOARD1:def_1;
then ( (X_axis f) . n = p `1 & (X_axis f) . n in rng (X_axis f) ) by A1, A3, FUNCT_1:def_3, GOBOARD1:def_1;
then consider i being Nat such that
A16: i in dom (Incr (X_axis f)) and
A17: (Incr (X_axis f)) . i = p `1 by A15, FINSEQ_2:10;
A18: p = |[(p `1),(p `2)]| by EUCLID:53;
len (Col ((GoB f),(width (GoB f)))) = len (GoB f) by MATRIX_1:def_8;
then A19: dom (Col ((GoB f),(width (GoB f)))) = dom (GoB f) by FINSEQ_3:29;
( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def_21;
then A20: dom (Incr (X_axis f)) = dom (GoB f) by FINSEQ_3:29;
A21: ( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def_21;
then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (Y_axis f)) = Seg (width (GoB f)) ) by FINSEQ_1:def_3, MATRIX_1:def_4;
then [i,(width (GoB f))] in Indices (GoB f) by A21, A16, A7, A20, A11, ZFMISC_1:87;
then (GoB f) * (i,(width (GoB f))) = |[(p `1),(p `2)]| by A21, A16, A17, A8, A11, Def1;
then (Col ((GoB f),(width (GoB f)))) . i = f /. n by A16, A20, A18, MATRIX_1:def_8;
hence f /. n in rng (Col ((GoB f),(width (GoB f)))) by A16, A20, A19, FUNCT_1:def_3; ::_thesis: verum
end;