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 vs is_vertex_seq_of c & e in rng c holds
( the Target of G . e in rng vs & the Source of G . e in rng vs )
let c be Chain of G; :: thesis: for vs being FinSequence of the carrier of G
for e being set st vs is_vertex_seq_of c & e in rng c holds
( the Target of G . e in rng vs & the Source of G . e in rng vs )
let vs be FinSequence of the carrier of G; :: thesis: for e being set st vs is_vertex_seq_of c & e in rng c holds
( the Target of G . e in rng vs & the Source of G . e in rng vs )
let e be set ; :: thesis: ( vs is_vertex_seq_of c & e in rng c implies ( the Target of G . e in rng vs & the Source of G . e in rng vs ) )
assume A1: ( vs is_vertex_seq_of c & e in rng c ) ; :: thesis: ( the Target of G . e in rng vs & the Source of G . e in rng vs )
c is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then A2: rng c c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e' = e as Element of the carrier' of G by A1;
reconsider t = the Target of G . e, s = the Source of G . e as Vertex of G by A1, A2, FUNCT_2:7;
A3: e' in rng c by A1;
then A4: t in G -VSet (rng c) ;
s in G -VSet (rng c) by A3;
hence ( the Target of G . e in rng vs & the Source of G . e in rng vs ) by A1, A4, GRAPH_2:34, RELAT_1:60; :: thesis: verum