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
consider vs being FinSequence of the carrier of G such that
A1:
( vs is_vertex_seq_of sc & ( 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 q' = sc | (Seg n) as Chain of G by GRAPH_1:4;
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 A2:
1
<= k
and A3:
k < m
and A4:
m <= len p'
and A5:
p' . k = p' . m
;
:: thesis: ( k = 1 & m = len p' )
(
k <= len p' & 1
<= m )
by A2, A3, A4, XXREAL_0:2;
then A6:
(
p' . k = vs . k &
p' . m = vs . m )
by A2, A4, Th2;
A7:
len p' <= len vs
by Th2;
then A8:
m <= len vs
by A4, XXREAL_0:2;
hence
k = 1
by A1, A2, A3, A5, A6;
:: thesis: m = len p'
(
len p' = len vs or
len p' < len vs )
by A7, XXREAL_0:1;
hence
m = len p'
by A1, A2, A3, A4, A5, A6, A8;
:: thesis: verum end;
hence
sc | (Seg n) is simple Chain of G
by Def10; :: thesis: verum