:: deftheorem Def2 defines PairF JGRAPH_1:def 2 :
for f, b₂ being FinSequence holds
( b₂ = PairF f iff ( len b₂ = (len f) -' 1 & ( for i being Nat st 1 <= i & i < len f holds
b₂ . i = [(f . i),(f . (i + 1))] ) ) );