let G be finite chordal _Graph; :: thesis:
let a, b be Vertex of G; :: thesis:
assume that
A1: a <> b and
A2: not a,b are_adjacent ; :: thesis:
let S be VertexSeparator of a,b; :: thesis:
assume A3: S is minimal ; :: thesis:
let H be removeVertices of G,S; :: thesis:
let a1 be Vertex of H; :: thesis:
assume A4: a = a1 ; :: thesis:
assume A5: for c being Vertex of G holds
( not c in H .reachableFrom a1 or ex x being Vertex of G st
( x in S & not c,x are_adjacent ) ) ; :: thesis:

per cases ;

suppose S is empty ; :: thesis:

then for x being Vertex of G holds
( not x in S or a,x are_adjacent ) ;
then not a in H .reachableFrom a1 by A5;
hence contradiction by A4, GLIB_002:9; :: thesis:

end;

suppose not S is empty ; :: thesis:

then reconsider S = S as non empty Subset of (the_Vertices_of G) ;
set A = H .reachableFrom a1;
deffunc H₁( set ) -> Element of omega = card ((G .AdjacentSet {$1}) /\ S);
set M = { H₁(x) where x is Vertex of G : x in H .reachableFrom a1 } ;
a in H .reachableFrom a1 by A4, GLIB_002:9;
then A6: card ((G .AdjacentSet {a}) /\ S) in { H₁(x) where x is Vertex of G : x in H .reachableFrom a1 } ;
A7: H .reachableFrom a1 is finite ;
A8: { H₁(x) where x is Vertex of G : x in H .reachableFrom a1 } is finite from FRAENKEL:sch 21(A7);

now

let x be set ; :: thesis:
assume A9: x in { H₁(x) where x is Vertex of G : x in H .reachableFrom a1 } ; :: thesis:
consider y being Vertex of G such that
A10: x = card ((G .AdjacentSet {y}) /\ S) and
y in H .reachableFrom a1 by A9;
thus x is natural by A10; :: thesis:

end;

then reconsider M = { H₁(x) where x is Vertex of G : x in H .reachableFrom a1 } as non empty finite natural-membered set by A6, A8, MEMBERED:def 6;
max M in M by XXREAL_2:def 8;
then consider c being Vertex of G such that
A11: max M = card ((G .AdjacentSet {c}) /\ S) and
A12: c in H .reachableFrom a1 ;
consider y being Vertex of G such that
A13: y in S and
A14: not c,y are_adjacent by A5, A12;
A15: (H .reachableFrom a1) /\ S = {} by A1, A2, A4, Th75;
consider Ga being inducedSubgraph of H,(H .reachableFrom a1);
A16: the_Vertices_of Ga = H .reachableFrom a1 by GLIB_000:def 39;
set tVG = the_Vertices_of G;
the_Vertices_of H c= the_Vertices_of G ;
then reconsider A = H .reachableFrom a1 as non empty Subset of (the_Vertices_of G) by XBOOLE_1:1;
not a in S by A1, A2, Def8;
then A17: (the_Vertices_of G) \ S is non empty Subset of (the_Vertices_of G) by XBOOLE_0:def 5;

now

let x be set ; :: thesis:
assume A18: x in A ; :: thesis:
not x in S by A15, A18, XBOOLE_0:def 4;
hence x in (the_Vertices_of G) \ S by A18, XBOOLE_0:def 5; :: thesis:

end;

then A c= (the_Vertices_of G) \ S by TARSKI:def 3;
then reconsider Ga = Ga as inducedSubgraph of G,A by A17, Th29;
set Ay = A \/ {y};
consider Gay being inducedSubgraph of G,(A \/ {y});
A19: the_Vertices_of Gay = A \/ {y} by GLIB_000:def 39;
y in {y} by TARSKI:def 1;
then ( c in A \/ {y} & y in A \/ {y} ) by A12, XBOOLE_0:def 3;
then reconsider ca = c, ya = y as Vertex of Gay by GLIB_000:def 39;
consider yaa being Vertex of G such that
A20: yaa in A and
A21: y,yaa are_adjacent by A1, A2, A3, A4, A13, Th82;
not y in A by A13, A15, XBOOLE_0:def 4;
then y in G .AdjacentSet (the_Vertices_of Ga) by A16, A20, A21;
then Gay is connected by Th57;
then consider Wa being Walk of Gay such that
A22: Wa is_Walk_from ca,ya by GLIB_002:def 1;
A23: ( Wa .first() = ca & Wa .last() = ya ) by A22, GLIB_001:def 23;
consider P being Path of Gay such that
A24: P is_Walk_from Wa .first() ,Wa .last() and
A25: P is minlength by Th39;
A26: P .first() = ca by A23, A24, GLIB_001:def 23;
A27: P .last() = y by A23, A24, GLIB_001:def 23;
c <> y by A12, A13, A15, XBOOLE_0:def 4;
then not P is trivial by A26, A27, GLIB_001:128;
then A28: len P >= 3 by GLIB_001:126;

A29: now

assume len P < (2 * 2) + 1 ; :: thesis:
then len P <= 5 - 2 by Th3;
then A30: len P = 3 by A28, XXREAL_0:1;
then (2 * 0 ) + 1 < len P ;
then P . (1 + 1) Joins P . 1,P . (1 + 2),Gay by GLIB_001:def 3;
then P . 2 Joins c,y,G by A26, A27, A30, GLIB_000:75;
hence contradiction by A14, Def3; :: thesis:

end;

then 5 + (- 2) <= (len P) + (- 2) by XREAL_1:9;
then reconsider j = (len P) - (2 * 1) as odd Element of NAT by INT_1:16, XXREAL_0:2;
set d = P . j;
A31: j < len P by XREAL_1:46;
then A32: P . j in the_Vertices_of Gay by GLIB_001:8;
then A33: ( P . j in A or P . j in {y} ) by A19, XBOOLE_0:def 3;

A34: now

assume P . j = y ; :: thesis:
then (len P) - 2 = 1 by A27, A31, GLIB_001:def 28;
then ( len P = 1 + 2 & 3 < 5 ) ;
hence contradiction by A29; :: thesis:

end;

reconsider d = P . j as Vertex of G by A32;
P . (j + 1) Joins d,P . (((len P) - 2) + 2),Gay by A31, GLIB_001:def 3;
then A35: P . (j + 1) Joins d,y,G by A27, GLIB_000:75;
then ( d <> y & d,y are_adjacent ) by A34, Def3;
then A36: y in G .AdjacentSet {d} by Th52;
then A37: y in (G .AdjacentSet {d}) /\ S by A13, XBOOLE_0:def 4;
A38: not y in G .AdjacentSet {c} by A14, Th52;
set gds = (G .AdjacentSet {d}) /\ S;
set gcs = (G .AdjacentSet {c}) /\ S;

now

assume A39: (G .AdjacentSet {c}) /\ S c= (G .AdjacentSet {d}) /\ S ; :: thesis:
not y in (G .AdjacentSet {c}) /\ S by A38, XBOOLE_0:def 4;
then (G .AdjacentSet {c}) /\ S c< (G .AdjacentSet {d}) /\ S by A37, A39, XBOOLE_0:def 8;
then A40: card ((G .AdjacentSet {c}) /\ S) < card ((G .AdjacentSet {d}) /\ S) by TREES_1:24;
card ((G .AdjacentSet {d}) /\ S) in M by A33, A34, TARSKI:def 1;
hence contradiction by A11, A40, XXREAL_2:def 8; :: thesis:

end;

then consider x being set such that
A41: x in (G .AdjacentSet {c}) /\ S and
A42: not x in (G .AdjacentSet {d}) /\ S by TARSKI:def 3;
A43: x in S by A41, XBOOLE_0:def 4;
then A44: not x in G .AdjacentSet {d} by A42, XBOOLE_0:def 4;
reconsider x = x as Vertex of G by A41;
A45: x <> y by A13, A36, A42, XBOOLE_0:def 4;
consider Gs being inducedSubgraph of G,S;
reconsider xs = x, ys = y as Vertex of Gs by A13, A43, GLIB_000:def 39;
Gs is complete by A1, A2, A3, Th98;
then xs,ys are_adjacent by A45, Def6;
then consider ej being set such that
A46: ej Joins xs,ys,Gs by Def3;
ej Joins x,y,G by A46, GLIB_000:75;
then A47: x,y are_adjacent by Def3;
x in G .AdjacentSet {c} by A41, XBOOLE_0:def 4;
then A48: c,x are_adjacent by Th52;
d <> x by A15, A33, A34, A43, TARSKI:def 1, XBOOLE_0:def 4;
then A49: not d,x are_adjacent by A44, Th52;
defpred S₁[ Nat] means ( $1 in dom P & not $1 is even & $1 < len P & ex e being set st e Joins x,P . $1,G );
A50: for k being Nat st S₁[k] holds
k <= len P ;
A51: 1 < len P by A29, XXREAL_0:2;
then A52: 1 in dom P by FINSEQ_3:27;
A53: not (2 * 0 ) + 1 is even ;
ex e being set st e Joins x,P . 1,G by A26, A48, Def3;
then A54: ex k being Nat st S₁[k] by A51, A52, A53;
consider k being Nat such that
A55: S₁[k] and
A56: for i being Nat st S₁[i] holds
k >= i from NAT_1:sch 6(A50, A54);
reconsider k = k as odd Element of NAT by A55;
A57: ( k <= j & j < len P ) by A55, Th3, XREAL_1:46;
A58: P . k <> P . j by A49, A55, Def3;

A59: now

assume A60: P . k = P . (len P) ; :: thesis:
A61: ( (2 * 0 ) + 1 <= k & k <= len P ) by A55, HEYTING3:1;
then A62: P .cut 1,k is_Walk_from P .first() ,P .last() by A60, GLIB_001:38;
(len (P .cut 1,k)) + 1 = k + 1 by A61, GLIB_001:37;
hence contradiction by A25, A55, A62, Def2; :: thesis:

end;

set Q1 = P .cut k,j;
A63: P .cut k,j is minlength by A25, A57, Th42;
A64: ( (P .cut k,j) .first() = P . k & (P .cut k,j) .last() = P . j ) by A57, GLIB_001:38;
reconsider Q = P .cut k,j as Path of G by GLIB_001:176;
A65: Q .vertices() = (P .cut k,j) .vertices() by GLIB_001:99;
A66: Q .first() = P . k by A64;
A67: Q .last() = P . j by A64;
A68: Q .first() <> Q .last() by A49, A55, A64, Def3;
A69: not Q is trivial by A58, A66, A67, GLIB_001:128;
then ( Q .length() <> 0 & Q .length() >= 0 ) by GLIB_001:def 26;
then A70: Q .length() >= 0 + 1 by NAT_1:13;
A71: not Q is closed by A68, GLIB_001:def 24;
A72: (len Q) + k = j + 1 by A57, GLIB_001:37;
set cc = Q .first() ;
set dd = Q .last() ;
A73: ( not x in A & not x in {y} ) by A15, A43, A45, TARSKI:def 1, XBOOLE_0:def 4;
Q .last() in (P .cut k,j) .vertices() by A65, GLIB_001:89;
then A74: Q .last() <> x by A19, A73, XBOOLE_0:def 3;
Q .first() in (P .cut k,j) .vertices() by A65, GLIB_001:89;
then A75: Q .first() <> x by A19, A73, XBOOLE_0:def 3;
A76: Q .last() ,y are_adjacent by A35, A64, Def3;
A77: x,Q .first() are_adjacent by A55, A64, Def3;

A78: now

let i be odd Nat; :: thesis:
assume A79: ( i in dom Q & i <> len Q ) ; :: thesis:
assume ex e being set st e Joins Q . i,y,G ; :: thesis:
then consider e being set such that
A80: e Joins Q . i,y,G ;
A81: i <= len Q by A79, FINSEQ_3:27;
1 <= i by A79, FINSEQ_3:27;
then 1 + (- 1) <= i + (- 1) by XREAL_1:9;
then reconsider i1 = i - 1 as even Element of NAT by INT_1:16;
reconsider ki1 = k + i1 as odd Element of NAT ;
A82: i + (- 1) < i + (- 0 ) by XREAL_1:10;
then i1 < len Q by A81, XXREAL_0:2;
then A83: ( Q . (i1 + 1) = P . ki1 & ki1 in dom P ) by A57, GLIB_001:37;
then A84: ki1 <= len P by FINSEQ_3:27;

now

assume A85: ki1 = len P ; :: thesis:
((len P) - k) + (- 1) < (len P) - k by XREAL_1:32;
hence contradiction by A72, A81, A82, A85, XXREAL_0:2; :: thesis:

end;

then ki1 < len P by A84, XXREAL_0:1;
then A86: ki1 + 2 <= len P by Th4;
ki1 + 2 <> len P by A72, A79;
then A87: ki1 + 2 < len P by A86, XXREAL_0:1;
( P . ki1 in A \/ {y} & P . (len P) in A \/ {y} ) by A19, A84, GLIB_001:8;
hence contradiction by A25, A27, A80, A83, A87, Th19, Th40; :: thesis:

end;

A88: now

let i be odd Nat; :: thesis:
assume A89: ( i in dom Q & i <> 1 ) ; :: thesis:
assume ex e being set st e Joins Q . i,x,G ; :: thesis:
then consider e being set such that
A90: e Joins Q . i,x,G ;
A91: ( 1 <= i & i <= len Q ) by A89, FINSEQ_3:27;
then 1 + (- 1) <= i + (- 1) by XREAL_1:9;
then reconsider i1 = i - 1 as even Element of NAT by INT_1:16;
reconsider ki1 = k + i1 as odd Element of NAT ;
i + (- 1) < i + (- 0 ) by XREAL_1:10;
then A92: i1 < len Q by A91, XXREAL_0:2;
then A93: ( Q . (i1 + 1) = P . ki1 & ki1 in dom P ) by A57, GLIB_001:37;
A94: i1 + k < (((len P) - 1) - k) + k by A72, A92, XREAL_1:10;
(len P) + (- 1) < (len P) + (- 0 ) by XREAL_1:10;
then ( 1 <= ki1 & ki1 < len P ) by A94, HEYTING3:1, XXREAL_0:2;
then A95: ( ki1 in dom P & ki1 < len P ) by FINSEQ_3:27;

now

assume i1 <> 0 ; :: thesis:
then ( i1 <> 0 & i1 >= 0 ) ;
then k + 0 < k + i1 by XREAL_1:10;
hence contradiction by A56, A90, A93, A95, GLIB_000:17; :: thesis:

end;

hence contradiction by A89; :: thesis:

end;

A96: now

let v be set ; :: thesis:
assume A97: v in Q .vertices() ; :: thesis:
Q .vertices() c= P .vertices() by A57, A65, GLIB_001:95;
then A98: v in P .vertices() by A97;
consider n being odd Element of NAT such that
A99: ( n <= len Q & Q . n = v ) by A97, GLIB_001:88;
1 <= n by HEYTING3:1;
then 1 + (- 1) <= n + (- 1) by XREAL_1:9;
then reconsider n1 = n - 1 as even Element of NAT by INT_1:16;
reconsider kn1 = k + n1 as odd Element of NAT ;
n + (- 1) < n + (- 0 ) by XREAL_1:10;
then A100: n1 < len Q by A99, XXREAL_0:2;
then A101: ( Q . (n1 + 1) = P . kn1 & kn1 in dom P ) by A57, GLIB_001:37;
A102: k + n1 < (((len P) - 1) - k) + k by A72, A100, XREAL_1:10;
(len P) + (- 1) < (len P) + (- 0 ) by XREAL_1:10;
then A103: kn1 < len P by A102, XXREAL_0:2;

now

assume A104: v = y ; :: thesis:
then A105: k + (n + (- 1)) = 1 by A27, A99, A101, A103, GLIB_001:def 28;
A106: ( 1 <= k & 1 <= n ) by HEYTING3:1;

now

assume 1 < n ; :: thesis:
then 1 + 1 <= n by NAT_1:13;
then 2 + 1 <= k + n by A106, XREAL_1:9;
hence contradiction by A105; :: thesis:

end;

hence contradiction by A27, A59, A64, A99, A104, A106, XXREAL_0:1; :: thesis:

end;

then not v in {y} by TARSKI:def 1;
hence v in A by A19, A98, XBOOLE_0:def 3; :: thesis:

end;

consider R being Path of G such that
A107: ( len R = 7 & R .length() = 3 ) and
A108: R .vertices() = {(Q .last() ),y,x,(Q .first() )} and
A109: ( R . 1 = Q .last() & R . 3 = y & R . 5 = x & R . 7 = Q .first() ) by A27, A34, A45, A47, A59, A64, A74, A75, A76, A77, Th48;
A110: R .first() = Q .last() by A109;
A111: R .last() = Q .first() by A107, A109;
A112: not R is trivial by A107, GLIB_001:127;
A113: not R is closed by A68, A110, A111, GLIB_001:def 24;
A114: Q .edges() misses R .edges()

proof

assume not Q .edges() misses R .edges() ; :: thesis:
then (Q .edges() ) /\ (R .edges() ) <> {} by XBOOLE_0:def 7;
then consider e being set such that
A115: e in (Q .edges() ) /\ (R .edges() ) by XBOOLE_0:def 1;
A116: e in Q .edges() by A115, XBOOLE_0:def 4;
e in R .edges() by A115, XBOOLE_0:def 4;
then consider n being even Element of NAT such that
A117: ( 1 <= n & n <= 7 & R . n = e ) by A107, GLIB_001:100;

per cases by A117, Th13;

suppose A118: n = 2 ; :: thesis:

(2 * 0 ) + 1 < len R by A107;
then R . (1 + 1) Joins R . 1,R . (1 + 2),G by GLIB_001:def 3;
then y in Q .vertices() by A109, A116, A117, A118, GLIB_001:106;
then y in A by A96;
hence contradiction by A13, A15, XBOOLE_0:def 4; :: thesis:

end;

suppose A119: n = 4 ; :: thesis:

(2 * 1) + 1 < len R by A107;
then R . (3 + 1) Joins R . 3,R . (3 + 2),G by GLIB_001:def 3;
then y in Q .vertices() by A109, A116, A117, A119, GLIB_001:106;
then y in A by A96;
hence contradiction by A13, A15, XBOOLE_0:def 4; :: thesis:

end;

suppose A120: n = 6 ; :: thesis:

(2 * 2) + 1 < len R by A107;
then R . (5 + 1) Joins R . 5,R . (5 + 2),G by GLIB_001:def 3;
then x in Q .vertices() by A109, A116, A117, A120, GLIB_001:106;
then x in A by A96;
hence contradiction by A15, A43, XBOOLE_0:def 4; :: thesis:

end;

now

let v be set ; :: thesis:
assume A121: v in (Q .vertices() ) /\ (R .vertices() ) ; :: thesis:
v in Q .vertices() by A121, XBOOLE_0:def 4;
then A122: v in A by A96;
v in {(Q .last() ),y,x,(Q .first() )} by A108, A121, XBOOLE_0:def 4;
then ( v = Q .last() or v = y or v = x or v = Q .first() ) by ENUMSET1:def 2;
hence v in {(Q .first() ),(Q .last() )} by A13, A15, A43, A122, TARSKI:def 2, XBOOLE_0:def 4; :: thesis:

end;

then A123: (Q .vertices() ) /\ (R .vertices() ) c= {(Q .first() ),(Q .last() )} by TARSKI:def 3;

now

let v be set ; :: thesis:
assume A124: v in {(Q .first() ),(Q .last() )} ; :: thesis:

per cases by A124, TARSKI:def 2;

suppose A125: v = Q .first() ; :: thesis:

then A126: v in Q .vertices() by GLIB_001:89;
v in R .vertices() by A107, A109, A125, GLIB_001:88;
hence v in (Q .vertices() ) /\ (R .vertices() ) by A126, XBOOLE_0:def 4; :: thesis:

end;

suppose A127: v = Q .last() ; :: thesis:

then A128: v in Q .vertices() by GLIB_001:89;
(2 * 0 ) + 1 <= len R by A107;
then v in R .vertices() by A109, A127, GLIB_001:88;
hence v in (Q .vertices() ) /\ (R .vertices() ) by A128, XBOOLE_0:def 4; :: thesis:

end;

then {(Q .first() ),(Q .last() )} c= (Q .vertices() ) /\ (R .vertices() ) by TARSKI:def 3;
then A129: (Q .vertices() ) /\ (R .vertices() ) = {(Q .first() ),(Q .last() )} by A123, XBOOLE_0:def 10;
set C = Q .append R;
A130: Q .append R is Cycle-like by A69, A71, A110, A111, A112, A113, A114, A129, Th27;
A131: ((len (Q .append R)) + 1) + (- 1) = ((len Q) + (len R)) + (- 1) by A110, GLIB_001:29;
A132: (Q .append R) . ((len Q) + 6) = R . (6 + 1) by A107, A110, GLIB_001:34;
A133: (Q .append R) . ((len Q) + 4) = R . (4 + 1) by A107, A110, GLIB_001:34;
A134: (Q .append R) . ((len Q) + 2) = R . (2 + 1) by A107, A110, GLIB_001:34;
(Q .append R) .length() = (Q .length() ) + 3 by A107, A110, Th28;
then (Q .append R) .length() >= 1 + 3 by A70, XREAL_1:9;
then (Q .append R) .length() > 3 by NAT_1:13;
then Q .append R is chordal by A130, Def11;
then consider m, n being odd Nat such that
A135: m + 2 < n and
A136: n <= len (Q .append R) and
(Q .append R) . m <> (Q .append R) . n and
A137: ex e being set st e Joins (Q .append R) . m,(Q .append R) . n,G and
A138: ( Q .append R is Cycle-like implies ( ( not m = 1 or not n = len (Q .append R) ) & ( not m = 1 or not n = (len (Q .append R)) - 2 ) & ( not m = 3 or not n = len (Q .append R) ) ) ) by Th84;
A139: 1 <= m by HEYTING3:1;
A140: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )

proof

per cases ;

suppose n <= len Q ; :: thesis:

hence ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 ) ; :: thesis:

end;

suppose n > len Q ; :: thesis:

then A141: (len Q) + 2 <= n by Th4;

per cases ) + 2 = n or (len Q) + 2 < n ) by A141, XXREAL_0:1;

suppose (len Q) + 2 = n ; :: thesis:

hence ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 ) ; :: thesis:

end;

suppose (len Q) + 2 < n ; :: thesis:

then A142: ((len Q) + 2) + 2 <= n by Th4;

per cases ) + 4 = n or (len Q) + (2 * 2) < n ) by A142, XXREAL_0:1;

suppose (len Q) + 4 = n ; :: thesis:

hence ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 ) ; :: thesis:

end;

suppose (len Q) + (2 * 2) < n ; :: thesis:

then ((len Q) + 4) + 2 <= n by Th4;
hence ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 ) by A107, A131, A136, XXREAL_0:1; :: thesis:

end;

consider e being set such that
A143: e Joins (Q .append R) . m,(Q .append R) . n,G by A137;

per cases by A140;

suppose A144: n <= len Q ; :: thesis:

1 <= n by HEYTING3:1;
then A145: n in dom Q by A144, FINSEQ_3:27;
( m + 2 <= len Q & m + 0 <= m + 2 ) by A135, A144, XREAL_1:9, XXREAL_0:2;
then m <= len Q by XXREAL_0:2;
then m in dom Q by A139, FINSEQ_3:27;
then ( Q . m = (Q .append R) . m & Q . n = (Q .append R) . n ) by A145, GLIB_001:33;
hence contradiction by A63, A135, A143, A144, Th41; :: thesis:

end;

suppose A146: n = (len Q) + 2 ; :: thesis:

then m < len Q by A135, XREAL_1:8;
then A147: m in dom Q by A139, FINSEQ_3:27;
then e Joins Q . m,y,G by A109, A134, A143, A146, GLIB_001:33;
hence contradiction by A78, A135, A146, A147; :: thesis:

end;

suppose A148: n = (len Q) + 4 ; :: thesis:

then (m + 2) + 2 <= (len Q) + 4 by A135, Th4;
then m + 4 <= (len Q) + 4 ;
then m <= len Q by XREAL_1:8;
then A149: m in dom Q by A139, FINSEQ_3:27;
then A150: e Joins Q . m,x,G by A109, A133, A143, A148, GLIB_001:33;

per cases by A139, XXREAL_0:1;

suppose 1 = m ; :: thesis:

hence contradiction by A69, A71, A107, A110, A111, A112, A113, A114, A129, A131, A138, A148, Th27; :: thesis:

end;

suppose 1 < m ; :: thesis:

hence contradiction by A88, A149, A150; :: thesis:

end;

suppose A151: n = (len Q) + 6 ; :: thesis:

then (m + 2) + 2 <= (len Q) + 6 by A135, Th4;
then m + 4 <= ((len Q) + 2) + 4 ;
then A152: m <= (len Q) + 2 by XREAL_1:8;

per cases by A152, XXREAL_0:1;

suppose m < (len Q) + 2 ; :: thesis:

then A153: m <= len Q by Th4;
then m in dom Q by A139, FINSEQ_3:27;
then A154: (Q .append R) . m = Q . m by GLIB_001:33;

now

assume 1 + 2 >= m ; :: thesis:
then m < (2 * 1) + 1 by A69, A71, A107, A110, A111, A112, A113, A114, A129, A131, A138, A151, Th27, XXREAL_0:1;
then m <= 3 - 2 by Th3;
then m < 1 by A69, A71, A107, A110, A111, A112, A113, A114, A129, A131, A138, A151, Th27, XXREAL_0:1;
hence contradiction by HEYTING3:1; :: thesis:

end;

then ((2 * 0 ) + 1) + 2 < m ;
hence contradiction by A63, A109, A132, A143, A151, A153, A154, Th41, GLIB_000:17; :: thesis:

end;

suppose A155: m = (len Q) + 2 ; :: thesis:

( 3 <= len Q & 1 <= 3 ) by A69, GLIB_001:126;
then 1 <= len Q by XXREAL_0:2;
then ( (2 * 0 ) + 1 in dom Q & 1 <> len Q ) by A49, A55, A64, Def3, FINSEQ_3:27;
hence contradiction by A78, A109, A132, A134, A143, A151, A155, GLIB_000:17; :: thesis:

end;