let G be Graph; for c being Chain of G
for vs being FinSequence of the carrier of G
for e being set st e in the carrier' of G & vs is_vertex_seq_of c & vs . (len vs) = the Source of G . e holds
( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Target of G . e ) )
let c be Chain of G; for vs being FinSequence of the carrier of G
for e being set st e in the carrier' of G & vs is_vertex_seq_of c & vs . (len vs) = the Source of G . e holds
( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Target of G . e ) )
let vs be FinSequence of the carrier of G; for e being set st e in the carrier' of G & vs is_vertex_seq_of c & vs . (len vs) = the Source of G . e holds
( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Target of G . e ) )
let e be set ; ( e in the carrier' of G & vs is_vertex_seq_of c & vs . (len vs) = the Source of G . e implies ( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Target of G . e ) ) )
assume that
A1:
e in the carrier' of G
and
A2:
vs is_vertex_seq_of c
; ( not vs . (len vs) = the Source of G . e or ( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Target of G . e ) ) )
reconsider ec = <*e*> as Chain of G by A1, MSSCYC_1:5;
reconsider s = the Source of G . e, t = the Target of G . e as Vertex of G by A1, FUNCT_2:5;
reconsider vse = <*s,t*> as FinSequence of the carrier of G ;
A3:
( vse is_vertex_seq_of ec & vse . 1 = s )
by FINSEQ_1:44, MSSCYC_1:4;
assume A4:
vs . (len vs) = the Source of G . e
; ( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Target of G . e ) )
hence
c ^ <*e*> is Chain of G
by A2, A3, GRAPH_2:43; ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Target of G . e )
reconsider ce = c ^ ec as Chain of G by A2, A4, A3, GRAPH_2:43;
take vs9 = vs ^' vse; ( vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Target of G . e )
thus
vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*>
; ( vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Target of G . e )
vs9 is_vertex_seq_of ce
by A2, A4, A3, GRAPH_2:44;
hence
vs9 is_vertex_seq_of c ^ <*e*>
; ( vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Target of G . e )
len vs = (len c) + 1
by A2;
then
1 <= len vs
by NAT_1:11;
hence
vs9 . 1 = vs . 1
by FINSEQ_6:140; vs9 . (len vs9) = the Target of G . e
A5:
len vse = 2
by FINSEQ_1:44;
then
vse . (len vse) = t
by FINSEQ_1:44;
hence
vs9 . (len vs9) = the Target of G . e
by A5, FINSEQ_6:142; verum