let p, q be FinSequence; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 :: thesis: 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; :: thesis: ( 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; :: thesis: ( ( 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 :: thesis: 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 )

let n be Nat; :: thesis: ( 1 <= n & n <= len h2 implies h2 . n in the carrier of G )
assume that
A10: 1 <= n and
A11: n <= len h2 ; :: thesis: h2 . n in the carrier of G
n <= (len h1) + n by NAT_1:11;
then A12: 1 <= (len h1) + n by A10, XXREAL_0:2;
(len h1) + n <= (len h1) + (len h2) by A11, XREAL_1:7;
then A13: (len h1) + n <= len f by A8, FINSEQ_1:22;
n in dom h2 by A10, A11, FINSEQ_3:25;
then h2 . n = f . ((len h1) + n) by A8, FINSEQ_1:def 7;
hence h2 . n in the carrier of G by A3, A13, A12; :: thesis: verum

end;

hereby :: thesis: verum

let n be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: ( 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 ;
:: thesis: q . n joins x,y
thus q . n joins x,y by A14, A15, A18, Lm2; :: thesis: 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 :: thesis: 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; :: thesis: ( 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; :: thesis: ( ( 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 :: thesis: 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 )

let n be Nat; :: thesis: ( 1 <= n & n <= len f1 implies f1 . n in the carrier of G )
assume that
A23: 1 <= n and
A24: n <= len f1 ; :: thesis: f1 . n in the carrier of G
len f1 <= len f by A19, A20, NAT_1:11;
then n <= len f by A24, XXREAL_0:2;
then A25: f . n in the carrier of G by A3, A23;
n in dom f1 by A23, A24, FINSEQ_3:25;
hence f1 . n in the carrier of G by A21, A25, FINSEQ_1:def 7; :: thesis: verum

end;

hereby :: thesis: verum

let n be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: p . n joins x,y
thus p . n joins x,y by A26, A27, A30, Lm1; :: thesis: verum

end;

end;

A31: p is FinSequence of the carrier' of G by A1, FINSEQ_1:36;

now :: thesis: for n being Nat st 1 <= n & n <= len p holds
p . n in the carrier' of G

let n be Nat; :: thesis: ( 1 <= n & n <= len p implies p . n in the carrier' of G )
assume ( 1 <= n & n <= len p ) ; :: thesis: p . n in the carrier' of G
then n in dom p by FINSEQ_3:25;
hence p . n in the carrier' of G by A31, FINSEQ_2:11; :: thesis: verum

end;

hence p is Chain of G by A22, GRAPH_1:def 14; :: thesis: q is Chain of G
A32: q is FinSequence of the carrier' of G by A1, FINSEQ_1:36;

now :: thesis: for n being Nat st 1 <= n & n <= len q holds
q . n in the carrier' of G

let n be Nat; :: thesis: ( 1 <= n & n <= len q implies q . n in the carrier' of G )
assume ( 1 <= n & n <= len q ) ; :: thesis: q . n in the carrier' of G
then n in dom q by FINSEQ_3:25;
hence q . n in the carrier' of G by A32, FINSEQ_2:11; :: thesis: verum

end;

hence q is Chain of G by A9, GRAPH_1:def 14; :: thesis: verum