theorem Th2: :: PRVECT_3:2

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