let G be Graph; :: thesis: for pe, qe being FinSequence of the carrier' of G st rng qe c= rng pe holds
vertices qe c= vertices pe
let pe, qe be FinSequence of the carrier' of G; :: thesis: ( rng qe c= rng pe implies vertices qe c= vertices pe )
assume A1: rng qe c= rng pe ; :: thesis: vertices qe c= vertices pe
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in vertices qe or x in vertices pe )
assume x in vertices qe ; :: thesis: x in vertices pe
then consider v being Vertex of G such that
A2: x = v and
A3: ex i being Nat st
( i in dom qe & v in vertices (qe /. i) ) ;
consider i being Nat such that
A4: i in dom qe and
A5: v in vertices (qe /. i) by A3;
qe . i in rng qe by A4, FUNCT_1:def 3;
then consider j being object such that
A6: j in dom pe and
A7: qe . i = pe . j by A1, FUNCT_1:def 3;
reconsider j = j as Element of NAT by A6;
qe /. i = qe . i by A4, PARTFUN1:def 6;
then pe /. j = qe /. i by A6, A7, PARTFUN1:def 6;
hence x in vertices pe by A2, A5, A6; :: thesis: verum