theorem Th22: :: FUNCT_7:22

for p, q being FinSequence st len p = (len q) + 1 holds
for i being Nat holds
( i in dom q iff ( i in dom p & i + 1 in dom p ) )