let X be non empty set ; :: thesis: 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*> ) )
( dom <*X*> = {1} & <*X*> . 1 = X ) by FINSEQ_1:2, FINSEQ_1:38, FINSEQ_1:40;
hence 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*> ) ) by Th2; :: thesis: verum