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;

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 ) ) )

hence
sc | (Seg n) is simple Chain of G
by Def9; :: thesis: verum( 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;( 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