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 ) )
assume A1: p ^ q is Chain of G ; :: thesis: ( 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;
consider f being FinSequence such that
A2: ( len f = (len (p ^ q)) + 1 & ( for n being Element of NAT st 1 <= n & n <= len f holds
f . n in the carrier of G ) & ( for n being Element of 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 A1, GRAPH_1:def 12;
A3: ( p is FinSequence of the carrier' of G & q is FinSequence of the carrier' of G ) by A1, FINSEQ_1:50;

A4: now

let n be Element of 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:27;
hence p . n in the carrier' of G by A3, FINSEQ_2:13; :: thesis: verum

end;

A5: len (p ^ q) = (len p) + (len q) by FINSEQ_1:35;
then A6: len f = (len p) + ((len q) + 1) by A2;
A7: len f = ((len p) + 1) + (len q) by A2, A5;
then consider f1, f2 being FinSequence such that
A8: ( len f1 = (len p) + 1 & len f2 = len q & f = f1 ^ f2 ) by FINSEQ_2:25;

now

take f1 = f1; :: thesis: ( len f1 = (len p) + 1 & ( for n being Element of NAT st 1 <= n & n <= len f1 holds
f1 . n in the carrier of G ) & ( for n being Element of 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 A8; :: thesis: ( ( for n being Element of NAT st 1 <= n & n <= len f1 holds
f1 . n in the carrier of G ) & ( for n being Element of 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 Element of 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 Element of NAT ; :: thesis: ( 1 <= n & n <= len f1 implies f1 . n in the carrier of G )
assume A9: ( 1 <= n & n <= len f1 ) ; :: thesis: f1 . n in the carrier of G
len f1 <= len f by A7, A8, NAT_1:11;
then n <= len f by A9, XXREAL_0:2;
then A10: f . n in the carrier of G by A2, A9;
n in dom f1 by A9, FINSEQ_3:27;
hence f1 . n in the carrier of G by A8, A10, FINSEQ_1:def 7; :: thesis: verum

end;

hereby :: thesis: verum

let n be Element of 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 A11: ( 1 <= n & 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 A11, XXREAL_0:2;
then consider x, y being Element of the carrier of G such that
A12: ( x = f . n & y = f . (n + 1) & (p ^ q) . n joins x,y ) by A2, A11;
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 A8, NAT_1:11;
then n <= len f1 by A11, XXREAL_0:2;
hence x = f1 . n by A8, A11, A12, Lm1; :: thesis: ( y = f1 . (n + 1) & p . n joins x,y )
A13: 1 <= n + 1 by NAT_1:11;
n + 1 <= len f1 by A8, A11, XREAL_1:9;
then n + 1 in dom f1 by A13, FINSEQ_3:27;
hence y = f1 . (n + 1) by A8, A12, FINSEQ_1:def 7; :: thesis: p . n joins x,y
thus p . n joins x,y by A11, A12, Lm1; :: thesis: verum

end;

end;

hence p is Chain of G by A4, GRAPH_1:def 12; :: thesis: q is Chain of G

A14: now

let n be Element of 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:27;
hence q . n in the carrier' of G by A3, FINSEQ_2:13; :: thesis: verum

end;

consider h1, h2 being FinSequence such that
A15: ( len h1 = len p & len h2 = (len q) + 1 & f = h1 ^ h2 ) by A6, FINSEQ_2:25;

now

take h2 = h2; :: thesis: ( len h2 = (len q) + 1 & ( for n being Element of NAT st 1 <= n & n <= len h2 holds
h2 . n in the carrier of G ) & ( for n being Element of 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 A15; :: thesis: ( ( for n being Element of NAT st 1 <= n & n <= len h2 holds
h2 . n in the carrier of G ) & ( for n being Element of 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 Element of 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 Element of NAT ; :: thesis: ( 1 <= n & n <= len h2 implies h2 . n in the carrier of G )
assume A16: ( 1 <= n & n <= len h2 ) ; :: thesis: h2 . n in the carrier of G
then n in dom h2 by FINSEQ_3:27;
then A17: h2 . n = f . ((len h1) + n) by A15, FINSEQ_1:def 7;
(len h1) + n <= (len h1) + (len h2) by A16, XREAL_1:9;
then A18: (len h1) + n <= len f by A15, FINSEQ_1:35;
n <= (len h1) + n by NAT_1:11;
then 1 <= (len h1) + n by A16, XXREAL_0:2;
hence h2 . n in the carrier of G by A2, A17, A18; :: thesis: verum

end;

hereby :: thesis: verum

let n be Element of 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 A19: ( 1 <= n & 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;
A20: (len p) + n <= len (p ^ q) by A5, A19, XREAL_1:9;
n <= (len p) + n by NAT_1:11;
then 1 <= (len p) + n by A19, XXREAL_0:2;
then consider x, y being Element of the carrier of G such that
A21: ( x = f . ((len p) + n) & y = f . (((len p) + n) + 1) & (p ^ q) . ((len p) + n) joins x,y ) by A2, A20;
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 A15, NAT_1:11;
then n <= len h2 by A19, XXREAL_0:2;
hence x = h2 . n by A15, A19, A21, 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 A15, A19, Lm2, XREAL_1:9
.= y by A15, A21 ;
:: thesis: q . n joins x,y
thus q . n joins x,y by A19, A21, Lm2; :: thesis: verum

end;

end;

hence q is Chain of G by A14, GRAPH_1:def 12; :: thesis: verum