let p, q be FinSequence; :: thesis: for G being Graph st p ^ q is oriented Chain of G holds
( p is oriented Chain of G & q is oriented Chain of G )
let G be Graph; :: thesis: ( p ^ q is oriented Chain of G implies ( p is oriented Chain of G & q is oriented Chain of G ) )
assume A1: p ^ q is oriented Chain of G ; :: thesis: ( p is oriented Chain of G & q is oriented Chain of G )
set r = p ^ q;
A2: len (p ^ q) = (len p) + (len q) by FINSEQ_1:22;

A3: now :: thesis: for n being Nat st 1 <= n & n < len q holds
the Source of G . (q . (n + 1)) = the Target of G . (q . n)

let n be Nat; :: thesis: ( 1 <= n & n < len q implies the Source of G . (q . (n + 1)) = the Target of G . (q . n) )
assume that
A4: 1 <= n and
A5: n < len q ; :: thesis: the Source of G . (q . (n + 1)) = the Target of G . (q . n)
set m = (len p) + n;
n <= (len p) + n by NAT_1:11;
then A6: 1 <= (len p) + n by A4, XXREAL_0:2;
n + 1 <= len q by A5, NAT_1:13;
then A7: q . (n + 1) = (p ^ q) . ((len p) + (n + 1)) by Lm2, NAT_1:11
.= (p ^ q) . (((len p) + n) + 1) ;
(len p) + n < len (p ^ q) by A2, A5, XREAL_1:8;
then the Source of G . ((p ^ q) . (((len p) + n) + 1)) = the Target of G . ((p ^ q) . ((len p) + n)) by A1, A6, GRAPH_1:def 15;
hence the Source of G . (q . (n + 1)) = the Target of G . (q . n) by A4, A5, A7, Lm2; :: thesis: verum

end;

now :: thesis: for n being Nat st 1 <= n & n < len p holds
the Source of G . (p . (n + 1)) = the Target of G . (p . n)

let n be Nat; :: thesis: ( 1 <= n & n < len p implies the Source of G . (p . (n + 1)) = the Target of G . (p . n) )
assume that
A8: 1 <= n and
A9: n < len p ; :: thesis: the Source of G . (p . (n + 1)) = the Target of G . (p . n)
n + 1 <= len p by A9, NAT_1:13;
then A10: p . (n + 1) = (p ^ q) . (n + 1) by Lm1, NAT_1:11;
len p <= len (p ^ q) by A2, NAT_1:11;
then n < len (p ^ q) by A9, XXREAL_0:2;
then the Source of G . ((p ^ q) . (n + 1)) = the Target of G . ((p ^ q) . n) by A1, A8, GRAPH_1:def 15;
hence the Source of G . (p . (n + 1)) = the Target of G . (p . n) by A8, A9, A10, Lm1; :: thesis: verum

end;

hence ( p is oriented Chain of G & q is oriented Chain of G ) by A1, A3, Th8, GRAPH_1:def 15; :: thesis: verum