let n be Nat; for G being Graph
for sc being simple Chain of G holds sc | (Seg n) is simple Chain of G
let G be Graph; for sc being simple Chain of G holds sc | (Seg n) is simple Chain of G
let sc be simple Chain of G; sc | (Seg n) is simple Chain of G
reconsider q9 = sc | (Seg n) as Chain of G by GRAPH_1:4;
consider vs being FinSequence of the carrier of G such that
A1:
vs is_vertex_seq_of sc
and
A2:
for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )
by Def9;
reconsider p9 = vs | (Seg (n + 1)) as FinSequence of the carrier of G by FINSEQ_1:18;
now ex p9 being FinSequence of the carrier of G st
( p9 is_vertex_seq_of q9 & ( for k, m being Nat st 1 <= k & k < m & m <= len p9 & p9 . k = p9 . m holds
( k = 1 & m = len p9 ) ) )take p9 =
p9;
( p9 is_vertex_seq_of q9 & ( for k, m being Nat st 1 <= k & k < m & m <= len p9 & p9 . k = p9 . m holds
( k = 1 & m = len p9 ) ) )thus
p9 is_vertex_seq_of q9
by A1, Th40;
for k, m being Nat st 1 <= k & k < m & m <= len p9 & p9 . k = p9 . m holds
( k = 1 & m = len p9 )let k,
m be
Nat;
( 1 <= k & k < m & m <= len p9 & p9 . k = p9 . m implies ( k = 1 & m = len p9 ) )assume that A3:
1
<= k
and A4:
k < m
and A5:
m <= len p9
and A6:
p9 . k = p9 . m
;
( k = 1 & m = len p9 )
k <= len p9
by A4, A5, XXREAL_0:2;
then A7:
p9 . k = vs . k
by A3, FINSEQ_6:128;
1
<= m
by A3, A4, XXREAL_0:2;
then A8:
p9 . m = vs . m
by A5, FINSEQ_6:128;
A9:
len p9 <= len vs
by FINSEQ_6:128;
then A10:
m <= len vs
by A5, XXREAL_0:2;
hence
k = 1
by A2, A3, A4, A6, A7, A8;
m = len p9
(
len p9 = len vs or
len p9 < len vs )
by A9, XXREAL_0:1;
hence
m = len p9
by A2, A3, A4, A5, A6, A7, A8, A10;
verum end;
hence
sc | (Seg n) is simple Chain of G
by Def9; verum