theorem Th14: :: GRAPH_5:16

for G being Graph
for p being oriented Simple Chain of G
for q being FinSequence of the carrier' of G st len p >= 1 & len q = 1 & the Source of G . (q . 1) = the Target of G . (p . (len p)) & the Source of G . (p . 1) <> the Target of G . (p . (len p)) & ( for k being Nat holds
( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) holds
p ^ q is oriented Simple Chain of G