for X being non empty set
for f being FinSequence of X holds PairF f is FinSequence of the carrier' of (PGraph X)