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:35;

A3: now

let n be Element of NAT ; :: thesis: ( 1 <= n & n < len p implies the Source of G . (p . (n + 1)) = the Target of G . (p . n) )
assume A4: ( 1 <= n & n < len p ) ; :: thesis: the Source of G . (p . (n + 1)) = the Target of G . (p . n)
len p <= len (p ^ q) by A2, NAT_1:11;
then n < len (p ^ q) by A4, XXREAL_0:2;
then A5: the Source of G . ((p ^ q) . (n + 1)) = the Target of G . ((p ^ q) . n) by A1, A4, GRAPH_1:def 13;
n + 1 <= len p by A4, NAT_1:13;
then p . (n + 1) = (p ^ q) . (n + 1) by Lm1, NAT_1:11;
hence the Source of G . (p . (n + 1)) = the Target of G . (p . n) by A4, A5, Lm1; :: thesis: verum

end;

now

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

end;

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