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 that
A1: vs is_vertex_seq_of c and
A2: 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 A3: rng c c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e9 = e as Element of the carrier' of G by A2;
reconsider t = the Target of G . e, s = the Source of G . e as Vertex of G by A2, A3, FUNCT_2:5;
e9 in rng c by A2;
then ( t in G -VSet (rng c) & s in G -VSet (rng c) ) ;
hence ( the Target of G . e in rng vs & the Source of G . e in rng vs ) by A1, A2, GRAPH_2:31, RELAT_1:38; :: thesis: verum