let n be Nat; :: thesis: for G being Graph
for sc being simple Chain of G holds sc | (Seg n) is simple Chain of G
let G be Graph; :: thesis: for sc being simple Chain of G holds sc | (Seg n) is simple Chain of G
let sc be simple Chain of G; :: thesis: 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 :: thesis: 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; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

end;

hence sc | (Seg n) is simple Chain of G by Def9; :: thesis: verum