let G be Graph; for p, q being oriented Chain of G st the Target of G . (p . (len p)) = the Source of G . (q . 1) holds
p ^ q is oriented Chain of G
let p, q be oriented Chain of G; ( the Target of G . (p . (len p)) = the Source of G . (q . 1) implies p ^ q is oriented Chain of G )
assume A1:
the Target of G . (p . (len p)) = the Source of G . (q . 1)
; p ^ q is oriented Chain of G
per cases
( p = {} or q = {} or ( not p = {} & not q = {} ) )
;
suppose A3:
( not
p = {} & not
q = {} )
;
p ^ q is oriented Chain of Gconsider vs2 being
FinSequence of the
carrier of
G such that A4:
vs2 is_oriented_vertex_seq_of q
by GRAPH_4:9;
len vs2 = (len q) + 1
by A4, GRAPH_4:def 5;
then A5:
len vs2 >= 1
by NAT_1:12;
len q >= 1
by A3, FINSEQ_1:20;
then
q . 1
orientedly_joins vs2 /. 1,
vs2 /. (1 + 1)
by A4, GRAPH_4:def 5;
then A6: the
Source of
G . (q . 1) =
vs2 /. 1
by GRAPH_4:def 1
.=
vs2 . 1
by A5, FINSEQ_4:15
;
consider vs1 being
FinSequence of the
carrier of
G such that A7:
vs1 is_oriented_vertex_seq_of p
by GRAPH_4:9;
A8:
len vs1 = (len p) + 1
by A7, GRAPH_4:def 5;
then A9:
len vs1 >= 1
by NAT_1:12;
len p >= 1
by A3, FINSEQ_1:20;
then
p . (len p) orientedly_joins vs1 /. (len p),
vs1 /. ((len p) + 1)
by A7, GRAPH_4:def 5;
then the
Target of
G . (p . (len p)) =
vs1 /. (len vs1)
by A8, GRAPH_4:def 1
.=
vs1 . (len vs1)
by A9, FINSEQ_4:15
;
hence
p ^ q is
oriented Chain of
G
by A1, A7, A4, A6, GRAPH_4:14;
verum end;