theorem Th13: :: NTALGO_1:13
for b being FinSequence of INT st len b = 1 holds
Product b = b . 1