let p, q be FinSequence; for G being Graph st p ^ q is Chain of G holds
( p is Chain of G & q is Chain of G )
let G be Graph; ( p ^ q is Chain of G implies ( p is Chain of G & q is Chain of G ) )
set r = p ^ q;
set D = the carrier' of G;
set V = the carrier of G;
assume A1:
p ^ q is Chain of G
; ( p is Chain of G & q is Chain of G )
then consider f being FinSequence such that
A2:
len f = (len (p ^ q)) + 1
and
A3:
for n being Nat st 1 <= n & n <= len f holds
f . n in the carrier of G
and
A4:
for n being Nat st 1 <= n & n <= len (p ^ q) holds
ex x, y being Element of the carrier of G st
( x = f . n & y = f . (n + 1) & (p ^ q) . n joins x,y )
by GRAPH_1:def 14;
A5:
len (p ^ q) = (len p) + (len q)
by FINSEQ_1:22;
then
len f = (len p) + ((len q) + 1)
by A2;
then consider h1, h2 being FinSequence such that
A6:
len h1 = len p
and
A7:
len h2 = (len q) + 1
and
A8:
f = h1 ^ h2
by FINSEQ_2:22;
A9:
now ex h2 being FinSequence st
( len h2 = (len q) + 1 & ( for n being Nat st 1 <= n & n <= len h2 holds
h2 . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len q holds
ex x, y being Element of the carrier of G st
( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) ) )take h2 =
h2;
( len h2 = (len q) + 1 & ( for n being Nat st 1 <= n & n <= len h2 holds
h2 . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len q holds
ex x, y being Element of the carrier of G st
( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) ) )thus
len h2 = (len q) + 1
by A7;
( ( for n being Nat st 1 <= n & n <= len h2 holds
h2 . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len q holds
ex x, y being Element of the carrier of G st
( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) ) )hereby verum
let n be
Nat;
( 1 <= n & n <= len q implies ex x, y being Element of the carrier of G st
( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) )assume that A14:
1
<= n
and A15:
n <= len q
;
ex x, y being Element of the carrier of G st
( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y )set m =
(len p) + n;
n <= (len p) + n
by NAT_1:11;
then
1
<= (len p) + n
by A14, XXREAL_0:2;
then consider x,
y being
Element of the
carrier of
G such that A16:
x = f . ((len p) + n)
and A17:
y = f . (((len p) + n) + 1)
and A18:
(p ^ q) . ((len p) + n) joins x,
y
by A4, A5, A15, XREAL_1:7;
take x =
x;
ex y being Element of the carrier of G st
( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y )take y =
y;
( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y )
len q <= len h2
by A7, NAT_1:11;
then
n <= len h2
by A15, XXREAL_0:2;
hence
x = h2 . n
by A6, A8, A14, A16, Lm2;
( h2 . (n + 1) = y & q . n joins x,y )
1
<= n + 1
by NAT_1:11;
hence h2 . (n + 1) =
f . ((len h1) + (n + 1))
by A7, A8, A15, Lm2, XREAL_1:7
.=
y
by A6, A17
;
q . n joins x,ythus
q . n joins x,
y
by A14, A15, A18, Lm2;
verum
end; end;
A19:
len f = ((len p) + 1) + (len q)
by A2, A5;
then consider f1, f2 being FinSequence such that
A20:
len f1 = (len p) + 1
and
len f2 = len q
and
A21:
f = f1 ^ f2
by FINSEQ_2:22;
A22:
now ex f1 being FinSequence st
( len f1 = (len p) + 1 & ( for n being Nat st 1 <= n & n <= len f1 holds
f1 . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len p holds
ex x, y being Element of the carrier of G st
( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) ) )take f1 =
f1;
( len f1 = (len p) + 1 & ( for n being Nat st 1 <= n & n <= len f1 holds
f1 . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len p holds
ex x, y being Element of the carrier of G st
( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) ) )thus
len f1 = (len p) + 1
by A20;
( ( for n being Nat st 1 <= n & n <= len f1 holds
f1 . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len p holds
ex x, y being Element of the carrier of G st
( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) ) )hereby verum
let n be
Nat;
( 1 <= n & n <= len p implies ex x, y being Element of the carrier of G st
( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) )assume that A26:
1
<= n
and A27:
n <= len p
;
ex x, y being Element of the carrier of G st
( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y )
len p <= len (p ^ q)
by A5, NAT_1:11;
then
n <= len (p ^ q)
by A27, XXREAL_0:2;
then consider x,
y being
Element of the
carrier of
G such that A28:
x = f . n
and A29:
y = f . (n + 1)
and A30:
(p ^ q) . n joins x,
y
by A4, A26;
take x =
x;
ex y being Element of the carrier of G st
( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y )take y =
y;
( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y )
len p <= len f1
by A20, NAT_1:11;
then
n <= len f1
by A27, XXREAL_0:2;
hence
x = f1 . n
by A21, A26, A28, Lm1;
( y = f1 . (n + 1) & p . n joins x,y )
( 1
<= n + 1 &
n + 1
<= len f1 )
by A20, A27, NAT_1:11, XREAL_1:7;
then
n + 1
in dom f1
by FINSEQ_3:25;
hence
y = f1 . (n + 1)
by A21, A29, FINSEQ_1:def 7;
p . n joins x,ythus
p . n joins x,
y
by A26, A27, A30, Lm1;
verum
end; end;
A31:
p is FinSequence of the carrier' of G
by A1, FINSEQ_1:36;
hence
p is Chain of G
by A22, GRAPH_1:def 14; q is Chain of G
A32:
q is FinSequence of the carrier' of G
by A1, FINSEQ_1:36;
hence
q is Chain of G
by A9, GRAPH_1:def 14; verum