let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G
for v1, v2, v3 being Element 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 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 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 that
A1: len p >= 1 and
A2: p is_orientedpath_of v1,v2 and
A3: pe . 1 orientedly_joins v2,v3 and
A4: 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;
A5: pe is oriented Chain of G by A4, Th13;
( the Target of G . (p . (len p)) = v2 & the Source of G . (pe . 1) = v2 ) by A2, A3, GRAPH_4:def 1;
then reconsider q = p ^ pe as oriented Chain of G by A5, Th10;
A6: len q = (len p) + 1 by A4, FINSEQ_1:22;
the Target of G . (pe . 1) = v3 by A3, GRAPH_4:def 1;
then A7: the Target of G . (q . (len q)) = v3 by A4, A6, Lm2;
the Source of G . (p . 1) = v1 by A2;
then A8: the Source of G . (q . 1) = v1 by A1, Lm1;
take q ; :: thesis: ( q = p ^ pe & q is_orientedpath_of v1,v3 )
q <> {} by A6;
hence ( q = p ^ pe & q is_orientedpath_of v1,v3 ) by A8, A7; :: thesis: verum