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 ; :: 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 ;
then A7: p9 . k = vs . k by ;
1 <= m by ;
then A8: p9 . m = vs . m by ;
A9: len p9 <= len vs by FINSEQ_6:128;
then A10: m <= len vs by ;
hence k = 1 by A2, A3, A4, A6, A7, A8; :: thesis: m = len p9
( len p9 = len vs or len p9 < len vs ) by ;
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