for X being non empty set
for n being Nat
for f being FinSequence of X st 1 <= n & n <= len (PairF f) holds
(PairF f) . n in the carrier' of (PGraph X)