let G be Graph; :: thesis: 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 Target of G . e holds
( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Source of G . e ) )
let c be Chain of G; :: thesis: 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 Target of G . e holds
( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Source of G . e ) )
let vs be FinSequence of the carrier of G; :: thesis: for e being set st e in the carrier' of G & vs is_vertex_seq_of c & vs . (len vs) = the Target of G . e holds
( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Source of G . e ) )
let e be set ; :: thesis: ( e in the carrier' of G & vs is_vertex_seq_of c & vs . (len vs) = the Target of G . e implies ( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Source of G . e ) ) )
assume that
A1: e in the carrier' of G and
A2: vs is_vertex_seq_of c ; :: thesis: ( not vs . (len vs) = the Target of G . e or ( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Source 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:7;
assume A3: vs . (len vs) = the Target of G . e ; :: thesis: ( c ^ <*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Source of G . e ) )
reconsider vse = <*t,s*> as FinSequence of the carrier of G ;
A4: ( vse is_vertex_seq_of ec & vse . 1 = t ) by Th16, FINSEQ_1:61;
hence c ^ <*e*> is Chain of G by A2, A3, GRAPH_2:46; :: thesis: ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Source of G . e )
reconsider ce = c ^ ec as Chain of G by A2, A3, A4, GRAPH_2:46;
take vs9 = vs ^' vse; :: thesis: ( vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> & vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Source of G . e )
thus vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> ; :: thesis: ( vs9 is_vertex_seq_of c ^ <*e*> & vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Source of G . e )
vs9 is_vertex_seq_of ce by A2, A3, A4, GRAPH_2:47;
hence vs9 is_vertex_seq_of c ^ <*e*> ; :: thesis: ( vs9 . 1 = vs . 1 & vs9 . (len vs9) = the Source of G . e )
len vs = (len c) + 1 by A2, GRAPH_2:def 7;
then 1 <= len vs by NAT_1:11;
hence vs9 . 1 = vs . 1 by GRAPH_2:14; :: thesis: vs9 . (len vs9) = the Source of G . e
A5: len vse = 2 by FINSEQ_1:61;
then vse . (len vse) = s by FINSEQ_1:61;
hence vs9 . (len vs9) = the Source of G . e by A5, GRAPH_2:16; :: thesis: verum