let X, Y be non empty set ; :: thesis: ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x, y being set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) )
( dom <*X,Y*> = {1,2} & <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by FINSEQ_1:61, FINSEQ_1:4, FINSEQ_3:29;
hence ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x, y being set st x in X & y in Y holds
I . (x,y) = <*x,y*> ) ) by Th002; :: thesis: verum