let i be Nat; :: thesis: for G being Graph
for pe being FinSequence of the carrier' of G
for v being Element of G st i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds
v in vertices pe
let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G
for v being Element of G st i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds
v in vertices pe
let pe be FinSequence of the carrier' of G; :: thesis: for v being Element of G st i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds
v in vertices pe
let v be Element of G; :: thesis: ( i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) implies v in vertices pe )
set FS = the Source of G;
set FT = the Target of G;
assume that
A1: i in dom pe and
A2: ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) ; :: thesis: v in vertices pe
( v = the Source of G . (pe /. i) or v = the Target of G . (pe /. i) ) by A1, A2, PARTFUN1:def 6;
then v in vertices (pe /. i) by TARSKI:def 2;
hence v in vertices pe by A1; :: thesis: verum