let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G
for v1, v2, v3 being Element of the carrier of G
for p being oriented Chain of G st len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 holds
ex q being oriented Chain of G st
( q = p ^ pe & q is_orientedpath_of v1,v3 )
let pe be FinSequence of the carrier' of G; :: thesis: for v1, v2, v3 being Element of the carrier of G
for p being oriented Chain of G st len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 holds
ex q being oriented Chain of G st
( q = p ^ pe & q is_orientedpath_of v1,v3 )
let v1, v2, v3 be Element of the carrier of G; :: thesis: for p being oriented Chain of G st len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 holds
ex q being oriented Chain of G st
( q = p ^ pe & q is_orientedpath_of v1,v3 )
let p be oriented Chain of G; :: thesis: ( len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 implies ex q being oriented Chain of G st
( q = p ^ pe & q is_orientedpath_of v1,v3 ) )
assume A1: ( len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 ) ; :: thesis: ex q being oriented Chain of G st
( q = p ^ pe & q is_orientedpath_of v1,v3 )
set FT = the Target of G;
set FS = the Source of G;
A2: ( the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ) by A1, Def3;
A3: ( the Source of G . (pe . 1) = v2 & the Target of G . (pe . 1) = v3 ) by A1, GRAPH_4:def 1;
pe is oriented Chain of G by A1, Th18;
then reconsider q = p ^ pe as oriented Chain of G by A2, A3, Th15;
take q ; :: thesis: ( q = p ^ pe & q is_orientedpath_of v1,v3 )
A4: len q = (len p) + 1 by A1, FINSEQ_1:35;
then len q >= 1 by NAT_1:12;
then A5: q <> {} ;
A6: the Source of G . (q . 1) = v1 by A1, A2, Lm1;
the Target of G . (q . (len q)) = v3 by A1, A3, A4, Lm2;
hence ( q = p ^ pe & q is_orientedpath_of v1,v3 ) by A5, A6, Def3; :: thesis: verum