theorem Thm13: :: SRINGS_4:13

for X being 1 -element FinSequence st not X . 1 is empty holds
ex I being Function of (X . 1),(product X) st
( I is one-to-one & I is onto & ( for x being object st x in X . 1 holds
I . x = <*x*> ) )