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 set st x in X holds
I . x = <*x*> ) )
( dom <*X*> = {1} & <*X*> . 1 = X ) by FINSEQ_1:4, FINSEQ_1:55, FINSEQ_1:57;
hence ex I being Function of X,(product <*X*>) st
( I is one-to-one & I is onto & ( for x being set st x in X holds
I . x = <*x*> ) ) by Th002AA; :: thesis: verum