let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G
for p, q being oriented Chain of G st p = q ^ pe & len q >= 1 & len pe = 1 holds
vertices p = (vertices q) \/ {( the Target of G . (pe . 1))}
let pe be FinSequence of the carrier' of G; :: thesis: for p, q being oriented Chain of G st p = q ^ pe & len q >= 1 & len pe = 1 holds
vertices p = (vertices q) \/ {( the Target of G . (pe . 1))}
let p, q be oriented Chain of G; :: thesis: ( p = q ^ pe & len q >= 1 & len pe = 1 implies vertices p = (vertices q) \/ {( the Target of G . (pe . 1))} )
assume that
A1: p = q ^ pe and
A2: len q >= 1 and
A3: len pe = 1 ; :: thesis: vertices p = (vertices q) \/ {( the Target of G . (pe . 1))}
set FS = the Source of G;
set FT = the Target of G;
set V3 = {( the Target of G . (pe . 1))};
A4: len p = (len q) + 1 by A1, A3, FINSEQ_1:22;

now :: thesis: for x being object holds
( ( x in vertices p implies x in (vertices q) \/ {( the Target of G . (pe . 1))} ) & ( x in (vertices q) \/ {( the Target of G . (pe . 1))} implies x in vertices p ) )

let x be object ; :: thesis: ( ( x in vertices p implies x in (vertices q) \/ {( the Target of G . (pe . 1))} ) & ( x in (vertices q) \/ {( the Target of G . (pe . 1))} implies b₁ in vertices p ) )

hereby :: thesis: ( x in (vertices q) \/ {( the Target of G . (pe . 1))} implies b₁ in vertices p )

assume x in vertices p ; :: thesis: x in (vertices q) \/ {( the Target of G . (pe . 1))}
then consider y being Vertex of G such that
A5: y = x and
A6: ex i being Nat st
( i in dom p & y in vertices (p /. i) ) ;
consider i being Nat such that
A7: i in dom p and
A8: y in vertices (p /. i) by A6;
A9: 1 <= i by A7, FINSEQ_3:25;
A10: i <= len p by A7, FINSEQ_3:25;

per cases ( i <= len q or i > len q ) ;

suppose A11: i <= len q ; :: thesis: x in (vertices q) \/ {( the Target of G . (pe . 1))}

then A12: i in dom q by A9, FINSEQ_3:25;
p /. i = p . i by A9, A10, FINSEQ_4:15
.= q . i by A1, A9, A11, Lm1
.= q /. i by A9, A11, FINSEQ_4:15 ;
then y in { v where v is Vertex of G : ex j being Nat st
( j in dom q & v in vertices (q /. j) ) } by A8, A12;
hence x in (vertices q) \/ {( the Target of G . (pe . 1))} by A5, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A13: i > len q ; :: thesis: x in (vertices q) \/ {( the Target of G . (pe . 1))}

reconsider z = y as Vertex of G ;
i >= (len q) + 1 by A13, NAT_1:13;
then A14: i = (len q) + 1 by A4, A10, XXREAL_0:1;
A15: ( y = the Source of G . (p /. i) or y = the Target of G . (p /. i) ) by A8, TARSKI:def 2;

hereby :: thesis: verum

per cases ( z = the Source of G . (p . i) or z = the Target of G . (p . i) ) by A9, A10, A15, FINSEQ_4:15;

suppose A16: z = the Source of G . (p . i) ; :: thesis: x in (vertices q) \/ {( the Target of G . (pe . 1))}

len q < len p by A4, NAT_1:13;
then z = the Target of G . (p . (len q)) by A2, A14, A16, GRAPH_1:def 15
.= the Target of G . (q . (len q)) by A1, A2, Lm1
.= the Target of G . (q /. (len q)) by A2, FINSEQ_4:15 ;
then A17: z in vertices (q /. (len q)) by TARSKI:def 2;
len q in dom q by A2, FINSEQ_3:25;
then z in { v where v is Vertex of G : ex j being Nat st
( j in dom q & v in vertices (q /. j) ) } by A17;
hence x in (vertices q) \/ {( the Target of G . (pe . 1))} by A5, XBOOLE_0:def 3; :: thesis: verum

end;

suppose z = the Target of G . (p . i) ; :: thesis: x in (vertices q) \/ {( the Target of G . (pe . 1))}

then z = the Target of G . (pe . 1) by A1, A3, A14, Lm2;
then z in {( the Target of G . (pe . 1))} by TARSKI:def 1;
hence x in (vertices q) \/ {( the Target of G . (pe . 1))} by A5, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

end;

end;

end;

assume A18: x in (vertices q) \/ {( the Target of G . (pe . 1))} ; :: thesis: b₁ in vertices p

per cases ( x in vertices q or x in {( the Target of G . (pe . 1))} ) by A18, XBOOLE_0:def 3;

suppose A19: x in vertices q ; :: thesis: b₁ in vertices p

vertices q c= vertices p by A1, Th24;
hence x in vertices p by A19; :: thesis: verum

end;

suppose A20: x in {( the Target of G . (pe . 1))} ; :: thesis: b₁ in vertices p

1 in dom pe by A3, FINSEQ_3:25;
then reconsider y = the Target of G . (pe . 1) as Vertex of G by FINSEQ_2:11, FUNCT_2:5;
A21: 1 <= len p by A4, NAT_1:12;
then A22: len p in dom p by FINSEQ_3:25;
y = the Target of G . (p . (len p)) by A1, A3, A4, Lm2
.= the Target of G . (p /. (len p)) by A21, FINSEQ_4:15 ;
then A23: y in vertices (p /. (len p)) by TARSKI:def 2;
x = the Target of G . (pe . 1) by A20, TARSKI:def 1;
hence x in vertices p by A23, A22; :: thesis: verum

end;

end;

end;

hence vertices p = (vertices q) \/ {( the Target of G . (pe . 1))} by TARSKI:2; :: thesis: verum