let p, q be FinSequence; 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; ( 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
; ( 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 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;
( 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
;
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;
verum end;
hence
( p is oriented Chain of G & q is oriented Chain of G )
by A1, A3, Th8, GRAPH_1:def 15; verum