theorem Th3: :: COUSIN:4

for p being FinSequence
for i being Nat holds
( not i in dom p or i = 1 or 1 < i )