theorem Th4: :: PRVECT_3:4

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