let n be Element of 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 q' = 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 Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) by Def10;
reconsider p' = vs | (Seg (n + 1)) as FinSequence of the carrier of G by FINSEQ_1:23;

now

take p' = p'; :: thesis: ( p' is_vertex_seq_of q' & ( for k, m being Element of NAT st 1 <= k & k < m & m <= len p' & p' . k = p' . m holds
( k = 1 & m = len p' ) ) )
thus p' is_vertex_seq_of q' by A1, Th43; :: thesis: for k, m being Element of NAT st 1 <= k & k < m & m <= len p' & p' . k = p' . m holds
( k = 1 & m = len p' )
let k, m be Element of NAT ; :: thesis: ( 1 <= k & k < m & m <= len p' & p' . k = p' . m implies ( k = 1 & m = len p' ) )
assume that
A3: 1 <= k and
A4: k < m and
A5: m <= len p' and
A6: p' . k = p' . m ; :: thesis: ( k = 1 & m = len p' )
k <= len p' by A4, A5, XXREAL_0:2;
then A7: p' . k = vs . k by A3, Th2;
1 <= m by A3, A4, XXREAL_0:2;
then A8: p' . m = vs . m by A5, Th2;
A9: len p' <= len vs by Th2;
then A10: m <= len vs by A5, XXREAL_0:2;
hence k = 1 by A2, A3, A4, A6, A7, A8; :: thesis: m = len p'
( len p' = len vs or len p' < len vs ) by A9, XXREAL_0:1;
hence m = len p' by A2, A3, A4, A5, A6, A7, A8, A10; :: thesis: verum

end;

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