let n be Nat; for G being Graph
for p being Chain of G holds p | (Seg n) is Chain of G
let G be Graph; for p being Chain of G holds p | (Seg n) is Chain of G
let p be Chain of G; p | (Seg n) is Chain of G
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15;
A1:
for n being Nat st 1 <= n & n <= len q holds
q . n in the carrier' of G
ex q1 being FinSequence st
( len q1 = (len q) + 1 & ( for n being Nat st 1 <= n & n <= len q1 holds
q1 . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len q holds
ex x9, y9 being Vertex of G st
( x9 = q1 . n & y9 = q1 . (n + 1) & q . n joins x9,y9 ) ) )
proof
consider q1 being
FinSequence such that A5:
len q1 = (len p) + 1
and A6:
for
n being
Nat st 1
<= n &
n <= len q1 holds
q1 . n in the
carrier of
G
and A7:
for
n being
Nat st 1
<= n &
n <= len p holds
ex
x9,
y9 being
Vertex of
G st
(
x9 = q1 . n &
y9 = q1 . (n + 1) &
p . n joins x9,
y9 )
by Def14;
reconsider q2 =
q1 | (Seg (n + 1)) as
FinSequence by FINSEQ_1:15;
take
q2
;
( len q2 = (len q) + 1 & ( for n being Nat st 1 <= n & n <= len q2 holds
q2 . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len q holds
ex x9, y9 being Vertex of G st
( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 ) ) )
thus A8:
len q2 = (len q) + 1
( ( for n being Nat st 1 <= n & n <= len q2 holds
q2 . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len q holds
ex x9, y9 being Vertex of G st
( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 ) ) )
thus
for
n being
Nat st 1
<= n &
n <= len q2 holds
q2 . n in the
carrier of
G
for n being Nat st 1 <= n & n <= len q holds
ex x9, y9 being Vertex of G st
( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 )
let k be
Nat;
( 1 <= k & k <= len q implies ex x9, y9 being Vertex of G st
( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 ) )
assume that A19:
1
<= k
and A20:
k <= len q
;
ex x9, y9 being Vertex of G st
( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 )
A21:
k in dom q
by A19, A20, FINSEQ_3:25;
dom q c= dom p
by RELAT_1:60;
then
k <= len p
by A21, FINSEQ_3:25;
then consider x9,
y9 being
Vertex of
G such that A22:
x9 = q1 . k
and A23:
y9 = q1 . (k + 1)
and A24:
p . k joins x9,
y9
by A7, A19;
take
x9
;
ex y9 being Vertex of G st
( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 )
take
y9
;
( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 )
len q <= (len q) + 1
by NAT_1:11;
then
k <= len q2
by A8, A20, XXREAL_0:2;
then
k in dom q2
by A19, FINSEQ_3:25;
hence
x9 = q2 . k
by A22, FUNCT_1:47;
( y9 = q2 . (k + 1) & q . k joins x9,y9 )
A25:
k + 1
<= len q2
by A8, A20, XREAL_1:7;
1
+ 1
<= k + 1
by A19, XREAL_1:7;
then
1
<= k + 1
by XXREAL_0:2;
then
k + 1
in dom q2
by A25, FINSEQ_3:25;
hence
y9 = q2 . (k + 1)
by A23, FUNCT_1:47;
q . k joins x9,y9
thus
q . k joins x9,
y9
by A21, A24, FUNCT_1:47;
verum
end;
hence
p | (Seg n) is Chain of G
by A1, Def14; verum