let n be Element of NAT ; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ (Lower_Seq C,n) & p `1 = W-bound (L~ (Cage C,n)) holds
p = W-min (L~ (Cage C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st p in L~ (Lower_Seq C,n) & p `1 = W-bound (L~ (Cage C,n)) holds
p = W-min (L~ (Cage C,n))
let p be Point of (TOP-REAL 2); ( p in L~ (Lower_Seq C,n) & p `1 = W-bound (L~ (Cage C,n)) implies p = W-min (L~ (Cage C,n)) )
set Ca = Cage C,n;
set LS = Lower_Seq C,n;
set US = Upper_Seq C,n;
set Emax = E-max (L~ (Cage C,n));
set Nmin = N-min (L~ (Cage C,n));
set Nmax = N-max (L~ (Cage C,n));
set Wmax = W-max (L~ (Cage C,n));
set Wmin = W-min (L~ (Cage C,n));
set Ebo = E-bound (L~ (Cage C,n));
set Sbo = S-bound (L~ (Cage C,n));
set Wbo = W-bound (L~ (Cage C,n));
set Nbo = N-bound (L~ (Cage C,n));
set SW = SW-corner (L~ (Cage C,n));
assume that
A1:
p in L~ (Lower_Seq C,n)
and
A2:
p `1 = W-bound (L~ (Cage C,n))
and
A3:
p <> W-min (L~ (Cage C,n))
; contradiction
A4:
(Lower_Seq C,n) /. 1 = E-max (L~ (Cage C,n))
by JORDAN1F:6;
1 in dom (Lower_Seq C,n)
by FINSEQ_5:6;
then A5:
(Lower_Seq C,n) . 1 = E-max (L~ (Cage C,n))
by A4, PARTFUN1:def 8;
E-bound (L~ (Cage C,n)) <> W-bound (L~ (Cage C,n))
by SPRECT_1:33;
then
p <> (Lower_Seq C,n) . 1
by A2, A5, EUCLID:56;
then reconsider g1 = R_Cut (Lower_Seq C,n),p as being_S-Seq FinSequence of (TOP-REAL 2) by A1, JORDAN3:70;
len g1 in dom g1
by FINSEQ_5:6;
then A6: g1 /. (len g1) =
g1 . (len g1)
by PARTFUN1:def 8
.=
p
by A1, JORDAN3:59
;
reconsider g = Rev g1 as being_S-Seq FinSequence of (TOP-REAL 2) ;
<*p*> is_in_the_area_of Cage C,n
by A1, JORDAN1E:22, SPRECT_3:63;
then
g1 is_in_the_area_of Cage C,n
by A1, JORDAN1E:22, SPRECT_3:69;
then A7:
g is_in_the_area_of Cage C,n
by SPRECT_3:68;
A8:
g /. 1 = g1 /. (len g1)
by FINSEQ_5:68;
A9: g /. (len g) =
g /. (len g1)
by FINSEQ_5:def 3
.=
g1 /. 1
by FINSEQ_5:68
;
(g1 /. 1) `1 =
((Lower_Seq C,n) /. 1) `1
by A1, SPRECT_3:39
.=
(E-max (L~ (Cage C,n))) `1
by JORDAN1F:6
.=
E-bound (L~ (Cage C,n))
by EUCLID:56
;
then A10:
g is_a_h.c._for Cage C,n
by A2, A7, A8, A9, A6, SPRECT_2:def 2;
A11:
(Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n))
by JORDAN1F:5;
1 in dom (Upper_Seq C,n)
by FINSEQ_5:6;
then A12:
(Upper_Seq C,n) . 1 = W-min (L~ (Cage C,n))
by A11, PARTFUN1:def 8;
A13:
L~ g = L~ g1
by SPPOL_2:22;
len (Cage C,n) > 4
by GOBOARD7:36;
then A14:
rng (Cage C,n) c= L~ (Cage C,n)
by SPPOL_2:18, XXREAL_0:2;
now per cases
( W-min (L~ (Cage C,n)) <> SW-corner (L~ (Cage C,n)) or W-min (L~ (Cage C,n)) = SW-corner (L~ (Cage C,n)) )
;
suppose A15:
W-min (L~ (Cage C,n)) <> SW-corner (L~ (Cage C,n))
;
contradictionA16:
not
SW-corner (L~ (Cage C,n)) in rng (Cage C,n)
proof
A17:
(SW-corner (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n))
by EUCLID:56;
A18:
(SW-corner (L~ (Cage C,n))) `2 = S-bound (L~ (Cage C,n))
by EUCLID:56;
then
(SW-corner (L~ (Cage C,n))) `2 <= N-bound (L~ (Cage C,n))
by SPRECT_1:24;
then
SW-corner (L~ (Cage C,n)) in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = W-bound (L~ (Cage C,n)) & p1 `2 <= N-bound (L~ (Cage C,n)) & p1 `2 >= S-bound (L~ (Cage C,n)) ) }
by A17, A18;
then A19:
SW-corner (L~ (Cage C,n)) in LSeg (SW-corner (L~ (Cage C,n))),
(NW-corner (L~ (Cage C,n)))
by SPRECT_1:28;
assume
SW-corner (L~ (Cage C,n)) in rng (Cage C,n)
;
contradiction
then
SW-corner (L~ (Cage C,n)) in (LSeg (SW-corner (L~ (Cage C,n))),(NW-corner (L~ (Cage C,n)))) /\ (L~ (Cage C,n))
by A14, A19, XBOOLE_0:def 4;
then A20:
(SW-corner (L~ (Cage C,n))) `2 >= (W-min (L~ (Cage C,n))) `2
by PSCOMP_1:88;
A21:
(W-min (L~ (Cage C,n))) `1 = (SW-corner (L~ (Cage C,n))) `1
by PSCOMP_1:85;
(W-min (L~ (Cage C,n))) `2 >= (SW-corner (L~ (Cage C,n))) `2
by PSCOMP_1:87;
then
(W-min (L~ (Cage C,n))) `2 = (SW-corner (L~ (Cage C,n))) `2
by A20, XXREAL_0:1;
hence
contradiction
by A15, A21, TOPREAL3:11;
verum
end;
N-min (L~ (Cage C,n)) in rng (Upper_Seq C,n)
by Th7;
then
R_Cut (Upper_Seq C,n),
(N-min (L~ (Cage C,n))) = mid (Upper_Seq C,n),1,
((N-min (L~ (Cage C,n))) .. (Upper_Seq C,n))
by JORDAN1G:57;
then A22:
rng (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))) c= rng (Upper_Seq C,n)
by FINSEQ_6:125;
rng (Upper_Seq C,n) c= rng (Cage C,n)
by JORDAN1G:47;
then
rng (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))) c= rng (Cage C,n)
by A22, XBOOLE_1:1;
then
not
SW-corner (L~ (Cage C,n)) in rng (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))
by A16;
then
rng (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))) misses {(SW-corner (L~ (Cage C,n)))}
by ZFMISC_1:56;
then
rng (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))) misses rng <*(SW-corner (L~ (Cage C,n)))*>
by FINSEQ_1:55;
then A23:
rng (Rev (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))) misses rng <*(SW-corner (L~ (Cage C,n)))*>
by FINSEQ_5:60;
set h1 =
(Rev (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))) ^ <*(SW-corner (L~ (Cage C,n)))*>;
A24:
<*(SW-corner (L~ (Cage C,n)))*> is
one-to-one
by FINSEQ_3:102;
W-max (L~ (Cage C,n)) in L~ (Cage C,n)
by SPRECT_1:15;
then A25:
N-bound (L~ (Cage C,n)) >= (W-max (L~ (Cage C,n))) `2
by PSCOMP_1:71;
A26:
<*(SW-corner (L~ (Cage C,n)))*> is
special
;
A27:
N-min (L~ (Cage C,n)) in L~ (Upper_Seq C,n)
by Th7;
then
<*(N-min (L~ (Cage C,n)))*> is_in_the_area_of Cage C,
n
by JORDAN1E:21, SPRECT_3:63;
then
R_Cut (Upper_Seq C,n),
(N-min (L~ (Cage C,n))) is_in_the_area_of Cage C,
n
by A27, JORDAN1E:21, SPRECT_3:69;
then A28:
Rev (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))) is_in_the_area_of Cage C,
n
by SPRECT_3:68;
(W-max (L~ (Cage C,n))) `2 > (W-min (L~ (Cage C,n))) `2
by SPRECT_2:61;
then A29:
N-min (L~ (Cage C,n)) <> (Upper_Seq C,n) . 1
by A12, A25, EUCLID:56;
then reconsider RCutUS =
R_Cut (Upper_Seq C,n),
(N-min (L~ (Cage C,n))) as
being_S-Seq FinSequence of
(TOP-REAL 2) by A27, JORDAN3:70;
A30:
Rev RCutUS is
special
by SPPOL_2:42;
A31:
(Rev RCutUS) /. (len (Rev RCutUS)) =
(Rev RCutUS) /. (len RCutUS)
by FINSEQ_5:def 3
.=
RCutUS /. 1
by FINSEQ_5:68
.=
(Upper_Seq C,n) /. 1
by A27, SPRECT_3:39
.=
W-min (L~ (Cage C,n))
by JORDAN1F:5
;
then ((Rev RCutUS) /. (len (Rev RCutUS))) `1 =
W-bound (L~ (Cage C,n))
by EUCLID:56
.=
(SW-corner (L~ (Cage C,n))) `1
by EUCLID:56
.=
(<*(SW-corner (L~ (Cage C,n)))*> /. 1) `1
by FINSEQ_4:25
;
then reconsider h1 =
(Rev (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))) ^ <*(SW-corner (L~ (Cage C,n)))*> as
one-to-one special FinSequence of
(TOP-REAL 2) by A23, A24, A30, A26, FINSEQ_3:98, GOBOARD2:13;
set h =
Rev h1;
A32:
Rev h1 is
special
by SPPOL_2:42;
<*(SW-corner (L~ (Cage C,n)))*> is_in_the_area_of Cage C,
n
by SPRECT_2:32;
then
h1 is_in_the_area_of Cage C,
n
by A28, SPRECT_2:28;
then A33:
Rev h1 is_in_the_area_of Cage C,
n
by SPRECT_3:68;
L~ (Rev h1) = L~ h1
by SPPOL_2:22;
then A34:
L~ (Rev h1) = (L~ (Rev RCutUS)) \/ (LSeg ((Rev RCutUS) /. (len (Rev RCutUS))),(SW-corner (L~ (Cage C,n))))
by SPPOL_2:19;
A35:
(Index (N-min (L~ (Cage C,n))),(Upper_Seq C,n)) + 1
>= 0 + 1
by XREAL_1:9;
A36:
2
<= len g
by TOPREAL1:def 10;
len h1 =
(len (Rev (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))))) + 1
by FINSEQ_2:19
.=
(len (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))) + 1
by FINSEQ_5:def 3
.=
((Index (N-min (L~ (Cage C,n))),(Upper_Seq C,n)) + 1) + 1
by A27, A29, JORDAN3:60
;
then
len h1 >= 1
+ 1
by A35, XREAL_1:9;
then A37:
len (Rev h1) >= 2
by FINSEQ_5:def 3;
A38:
(Rev h1) /. 1
= h1 /. (len h1)
by FINSEQ_5:68;
A39:
len (Upper_Seq C,n) in dom (Upper_Seq C,n)
by FINSEQ_5:6;
1
in dom (Rev RCutUS)
by FINSEQ_5:6;
then h1 /. 1 =
(Rev RCutUS) /. 1
by FINSEQ_4:83
.=
(R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))) /. (len (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))))
by FINSEQ_5:68
.=
N-min (L~ (Cage C,n))
by A27, Th45
;
then A40:
(h1 /. 1) `2 = N-bound (L~ (Cage C,n))
by EUCLID:56;
A41:
(h1 /. (len h1)) `2 =
(h1 /. ((len (Rev (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))))) + 1)) `2
by FINSEQ_2:19
.=
(SW-corner (L~ (Cage C,n))) `2
by FINSEQ_4:82
.=
S-bound (L~ (Cage C,n))
by EUCLID:56
;
A42:
len (Lower_Seq C,n) in dom (Lower_Seq C,n)
by FINSEQ_5:6;
(Rev h1) /. (len (Rev h1)) =
(Rev h1) /. (len h1)
by FINSEQ_5:def 3
.=
h1 /. 1
by FINSEQ_5:68
;
then
Rev h1 is_a_v.c._for Cage C,
n
by A33, A40, A38, A41, SPRECT_2:def 3;
then
L~ g meets L~ (Rev h1)
by A10, A32, A36, A37, SPRECT_2:33;
then consider x being
set such that A43:
x in L~ g
and A44:
x in L~ (Rev h1)
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A43;
A45:
L~ RCutUS c= L~ (Upper_Seq C,n)
by Th7, JORDAN3:76;
A46:
L~ g c= L~ (Lower_Seq C,n)
by A1, A13, JORDAN3:76;
then A47:
x in L~ (Lower_Seq C,n)
by A43;
now per cases
( x in L~ (Rev RCutUS) or x in LSeg ((Rev RCutUS) /. (len (Rev RCutUS))),(SW-corner (L~ (Cage C,n))) )
by A44, A34, XBOOLE_0:def 3;
suppose
x in L~ (Rev RCutUS)
;
contradictionthen A48:
x in L~ RCutUS
by SPPOL_2:22;
then
x in (L~ (Lower_Seq C,n)) /\ (L~ (Upper_Seq C,n))
by A43, A46, A45, XBOOLE_0:def 4;
then A49:
x in {(E-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))}
by JORDAN1E:20;
now per cases
( x = E-max (L~ (Cage C,n)) or x = W-min (L~ (Cage C,n)) )
by A49, TARSKI:def 2;
suppose
x = E-max (L~ (Cage C,n))
;
contradictionthen
(Upper_Seq C,n) /. (len (Upper_Seq C,n)) in L~ (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))
by A48, JORDAN1F:7;
then
(Upper_Seq C,n) . (len (Upper_Seq C,n)) in L~ (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))
by A39, PARTFUN1:def 8;
then
(Upper_Seq C,n) . (len (Upper_Seq C,n)) = N-min (L~ (Cage C,n))
by A27, Th43;
then
(Upper_Seq C,n) /. (len (Upper_Seq C,n)) = N-min (L~ (Cage C,n))
by A39, PARTFUN1:def 8;
then A50:
E-max (L~ (Cage C,n)) = N-min (L~ (Cage C,n))
by JORDAN1F:7;
N-max (L~ (Cage C,n)) in L~ (Cage C,n)
by SPRECT_1:13;
then A51:
E-bound (L~ (Cage C,n)) >= (N-max (L~ (Cage C,n))) `1
by PSCOMP_1:71;
(N-max (L~ (Cage C,n))) `1 > (N-min (L~ (Cage C,n))) `1
by SPRECT_2:55;
hence
contradiction
by A50, A51, EUCLID:56;
verum end; suppose
x = W-min (L~ (Cage C,n))
;
contradictionthen
(Lower_Seq C,n) /. (len (Lower_Seq C,n)) in L~ (R_Cut (Lower_Seq C,n),p)
by A13, A43, JORDAN1F:8;
then
(Lower_Seq C,n) . (len (Lower_Seq C,n)) in L~ (R_Cut (Lower_Seq C,n),p)
by A42, PARTFUN1:def 8;
then
(Lower_Seq C,n) . (len (Lower_Seq C,n)) = p
by A1, Th43;
then
(Lower_Seq C,n) /. (len (Lower_Seq C,n)) = p
by A42, PARTFUN1:def 8;
hence
contradiction
by A3, JORDAN1F:8;
verum end; hence
contradiction
;
verum end; suppose A52:
x in LSeg ((Rev RCutUS) /. (len (Rev RCutUS))),
(SW-corner (L~ (Cage C,n)))
;
contradiction
(W-min (L~ (Cage C,n))) `2 >= (SW-corner (L~ (Cage C,n))) `2
by PSCOMP_1:87;
then A53:
(W-min (L~ (Cage C,n))) `2 >= x `2
by A31, A52, TOPREAL1:10;
A54:
(W-min (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n))
by EUCLID:56;
(SW-corner (L~ (Cage C,n))) `1 = W-bound (L~ (Cage C,n))
by EUCLID:56;
then A55:
x `1 = W-bound (L~ (Cage C,n))
by A31, A52, A54, GOBOARD7:5;
L~ (Cage C,n) = (L~ (Lower_Seq C,n)) \/ (L~ (Upper_Seq C,n))
by JORDAN1E:17;
then
L~ (Lower_Seq C,n) c= L~ (Cage C,n)
by XBOOLE_1:7;
then
x in W-most (L~ (Cage C,n))
by A47, A55, SPRECT_2:16;
then
x `2 >= (W-min (L~ (Cage C,n))) `2
by PSCOMP_1:88;
then
x `2 = (W-min (L~ (Cage C,n))) `2
by A53, XXREAL_0:1;
then
x = W-min (L~ (Cage C,n))
by A54, A55, TOPREAL3:11;
then
(Lower_Seq C,n) /. (len (Lower_Seq C,n)) in L~ (R_Cut (Lower_Seq C,n),p)
by A13, A43, JORDAN1F:8;
then
(Lower_Seq C,n) . (len (Lower_Seq C,n)) in L~ (R_Cut (Lower_Seq C,n),p)
by A42, PARTFUN1:def 8;
then
(Lower_Seq C,n) . (len (Lower_Seq C,n)) = p
by A1, Th43;
then
(Lower_Seq C,n) /. (len (Lower_Seq C,n)) = p
by A42, PARTFUN1:def 8;
hence
contradiction
by A3, JORDAN1F:8;
verum end; hence
contradiction
;
verum end; suppose A56:
W-min (L~ (Cage C,n)) = SW-corner (L~ (Cage C,n))
;
contradictionset h =
R_Cut (Upper_Seq C,n),
(N-min (L~ (Cage C,n)));
A57:
2
<= len g
by TOPREAL1:def 10;
W-max (L~ (Cage C,n)) in L~ (Cage C,n)
by SPRECT_1:15;
then A58:
N-bound (L~ (Cage C,n)) >= (W-max (L~ (Cage C,n))) `2
by PSCOMP_1:71;
A59:
N-min (L~ (Cage C,n)) in L~ (Upper_Seq C,n)
by Th7;
then
<*(N-min (L~ (Cage C,n)))*> is_in_the_area_of Cage C,
n
by JORDAN1E:21, SPRECT_3:63;
then A60:
R_Cut (Upper_Seq C,n),
(N-min (L~ (Cage C,n))) is_in_the_area_of Cage C,
n
by A59, JORDAN1E:21, SPRECT_3:69;
(W-max (L~ (Cage C,n))) `2 > (W-min (L~ (Cage C,n))) `2
by SPRECT_2:61;
then
N-min (L~ (Cage C,n)) <> (Upper_Seq C,n) . 1
by A12, A58, EUCLID:56;
then reconsider RCutUS =
R_Cut (Upper_Seq C,n),
(N-min (L~ (Cage C,n))) as
being_S-Seq FinSequence of
(TOP-REAL 2) by A59, JORDAN3:70;
A61:
len RCutUS >= 2
by TOPREAL1:def 10;
(R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))) /. (len (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))) = N-min (L~ (Cage C,n))
by A59, Th45;
then A62:
((R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))) /. (len (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))))) `2 = N-bound (L~ (Cage C,n))
by EUCLID:56;
RCutUS /. 1 =
(Upper_Seq C,n) /. 1
by A59, SPRECT_3:39
.=
W-min (L~ (Cage C,n))
by JORDAN1F:5
;
then
((R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n)))) /. 1) `2 = S-bound (L~ (Cage C,n))
by A56, EUCLID:56;
then
R_Cut (Upper_Seq C,n),
(N-min (L~ (Cage C,n))) is_a_v.c._for Cage C,
n
by A60, A62, SPRECT_2:def 3;
then
L~ g meets L~ (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))
by A10, A57, A61, SPRECT_2:33;
then consider x being
set such that A63:
x in L~ g
and A64:
x in L~ (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A63;
A65:
len (Lower_Seq C,n) in dom (Lower_Seq C,n)
by FINSEQ_5:6;
A66:
L~ g c= L~ (Lower_Seq C,n)
by A1, A13, JORDAN3:76;
A67:
len (Upper_Seq C,n) in dom (Upper_Seq C,n)
by FINSEQ_5:6;
L~ RCutUS c= L~ (Upper_Seq C,n)
by Th7, JORDAN3:76;
then
x in (L~ (Lower_Seq C,n)) /\ (L~ (Upper_Seq C,n))
by A63, A64, A66, XBOOLE_0:def 4;
then A68:
x in {(E-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))}
by JORDAN1E:20;
now per cases
( x = E-max (L~ (Cage C,n)) or x = W-min (L~ (Cage C,n)) )
by A68, TARSKI:def 2;
suppose
x = E-max (L~ (Cage C,n))
;
contradictionthen
(Upper_Seq C,n) /. (len (Upper_Seq C,n)) in L~ (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))
by A64, JORDAN1F:7;
then
(Upper_Seq C,n) . (len (Upper_Seq C,n)) in L~ (R_Cut (Upper_Seq C,n),(N-min (L~ (Cage C,n))))
by A67, PARTFUN1:def 8;
then
(Upper_Seq C,n) . (len (Upper_Seq C,n)) = N-min (L~ (Cage C,n))
by A59, Th43;
then
(Upper_Seq C,n) /. (len (Upper_Seq C,n)) = N-min (L~ (Cage C,n))
by A67, PARTFUN1:def 8;
then A69:
E-max (L~ (Cage C,n)) = N-min (L~ (Cage C,n))
by JORDAN1F:7;
N-max (L~ (Cage C,n)) in L~ (Cage C,n)
by SPRECT_1:13;
then A70:
E-bound (L~ (Cage C,n)) >= (N-max (L~ (Cage C,n))) `1
by PSCOMP_1:71;
(N-max (L~ (Cage C,n))) `1 > (N-min (L~ (Cage C,n))) `1
by SPRECT_2:55;
hence
contradiction
by A69, A70, EUCLID:56;
verum end; suppose
x = W-min (L~ (Cage C,n))
;
contradictionthen
(Lower_Seq C,n) /. (len (Lower_Seq C,n)) in L~ (R_Cut (Lower_Seq C,n),p)
by A13, A63, JORDAN1F:8;
then
(Lower_Seq C,n) . (len (Lower_Seq C,n)) in L~ (R_Cut (Lower_Seq C,n),p)
by A65, PARTFUN1:def 8;
then
(Lower_Seq C,n) . (len (Lower_Seq C,n)) = p
by A1, Th43;
then
(Lower_Seq C,n) /. (len (Lower_Seq C,n)) = p
by A65, PARTFUN1:def 8;
hence
contradiction
by A3, JORDAN1F:8;
verum end; hence
contradiction
;
verum end;
hence
contradiction
; verum