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 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; :: 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 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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)*> ; :: thesis: ( 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*> ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum