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 object 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:2, FINSEQ_1:89;
hence ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x, y being object st x in X & y in Y holds
I . (x,y) = <*x,y*> ) ) by Th3; :: thesis: verum