theorem Th3: :: INT_5:3

for fp being FinSequence of INT st len fp = 1 holds
Poly-INT fp = INT --> (fp . 1)