let G be Graph; :: thesis: for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe holds
vertices qe c= vertices pe
let qe, pe 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 set ; :: 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 & ex i being Element of NAT st
( i in dom qe & v in vertices (qe /. i) ) ) ;
consider i being Element of NAT such that
A3: ( i in dom qe & v in vertices (qe /. i) ) by A2;
A4: qe /. i = qe . i by A3, PARTFUN1:def 8;
qe . i in rng qe by A3, FUNCT_1:def 5;
then consider j being set such that
A5: ( j in dom pe & qe . i = pe . j ) by A1, FUNCT_1:def 5;
reconsider j = j as Element of NAT by A5;
pe /. j = qe /. i by A4, A5, PARTFUN1:def 8;
hence x in vertices pe by A2, A3, A5; :: thesis: verum