let X be non-empty non empty FinSequence; :: thesis: for Y being non empty set ex I being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st

( I is one-to-one & I is onto & ( for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) )

let Y be non empty set ; :: thesis: ex I being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st

( I is one-to-one & I is onto & ( for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) )

A1: product <*Y*> <> {}

A2: ( I is one-to-one & I is onto & ( for x, y being set st x in product X & y in Y holds

I . (x,y) = [x,<*y*>] ) ) by Th15;

<*Y*> is non-empty

consider J being Function of [:(product X),(product YY):],(product (X ^ YY)) such that

A3: ( J is one-to-one & J is onto & ( for x, y being FinSequence st x in product X & y in product YY holds

J . (x,y) = x ^ y ) ) by PRVECT_3:6;

set K = J * I;

reconsider K = J * I as Function of [:(product X),Y:],(product (X ^ <*Y*>)) ;

take K ; :: thesis: ( K is one-to-one & K is onto & ( for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) )

thus K is one-to-one by A2, A3; :: thesis: ( K is onto & ( for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) )

A4: rng J = product (X ^ <*Y*>) by A3, FUNCT_2:def 3;

rng I = [:(product X),(product <*Y*>):] by A2, FUNCT_2:def 3;

then rng (J * I) = J .: [:(product X),(product <*Y*>):] by RELAT_1:127

.= product (X ^ <*Y*>) by A4, RELSET_1:22 ;

hence K is onto by FUNCT_2:def 3; :: thesis: for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )

thus for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) :: thesis: verum

( I is one-to-one & I is onto & ( for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) )

let Y be non empty set ; :: thesis: ex I being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st

( I is one-to-one & I is onto & ( for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & I . (x,y) = x1 ^ y1 ) ) )

A1: product <*Y*> <> {}

proof

consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that
assume
product <*Y*> = {}
; :: thesis: contradiction

then {} in rng <*Y*> by CARD_3:26;

then {} in {Y} by FINSEQ_1:39;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then {} in rng <*Y*> by CARD_3:26;

then {} in {Y} by FINSEQ_1:39;

hence contradiction by TARSKI:def 1; :: thesis: verum

A2: ( I is one-to-one & I is onto & ( for x, y being set st x in product X & y in Y holds

I . (x,y) = [x,<*y*>] ) ) by Th15;

<*Y*> is non-empty

proof

then reconsider YY = <*Y*> as non-empty non empty FinSequence ;
assume
not <*Y*> is non-empty
; :: thesis: contradiction

then {} in rng <*Y*> by RELAT_1:def 9;

then {} in {Y} by FINSEQ_1:39;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then {} in rng <*Y*> by RELAT_1:def 9;

then {} in {Y} by FINSEQ_1:39;

hence contradiction by TARSKI:def 1; :: thesis: verum

consider J being Function of [:(product X),(product YY):],(product (X ^ YY)) such that

A3: ( J is one-to-one & J is onto & ( for x, y being FinSequence st x in product X & y in product YY holds

J . (x,y) = x ^ y ) ) by PRVECT_3:6;

set K = J * I;

reconsider K = J * I as Function of [:(product X),Y:],(product (X ^ <*Y*>)) ;

take K ; :: thesis: ( K is one-to-one & K is onto & ( for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) )

thus K is one-to-one by A2, A3; :: thesis: ( K is onto & ( for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) )

A4: rng J = product (X ^ <*Y*>) by A3, FUNCT_2:def 3;

rng I = [:(product X),(product <*Y*>):] by A2, FUNCT_2:def 3;

then rng (J * I) = J .: [:(product X),(product <*Y*>):] by RELAT_1:127

.= product (X ^ <*Y*>) by A4, RELSET_1:22 ;

hence K is onto by FUNCT_2:def 3; :: thesis: for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )

thus for x, y being set st x in product X & y in Y holds

ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) :: thesis: verum

proof

let x, y be set ; :: thesis: ( x in product X & y in Y implies ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) )

assume A5: ( x in product X & y in Y ) ; :: thesis: ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )

then A6: I . (x,y) = [x,<*y*>] by A2;

A7: [x,y] in [:(product X),Y:] by A5, ZFMISC_1:87;

then [x,<*y*>] in [:(product X),(product <*Y*>):] by A6, A1, FUNCT_2:5;

then A8: <*y*> in product <*Y*> by ZFMISC_1:87;

reconsider xx = x as Function by A5;

dom xx = dom X by CARD_3:9, A5

.= Seg (len X) by FINSEQ_1:def 3 ;

then reconsider x1 = xx as FinSequence by FINSEQ_1:def 2;

set y1 = <*y*>;

A9: J . (x,<*y*>) = x1 ^ <*y*> by A3, A5, A8;

J . (x,<*y*>) = K . (x,y) by A6, A7, FUNCT_2:15;

hence ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) by A9; :: thesis: verum

end;( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) )

assume A5: ( x in product X & y in Y ) ; :: thesis: ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )

then A6: I . (x,y) = [x,<*y*>] by A2;

A7: [x,y] in [:(product X),Y:] by A5, ZFMISC_1:87;

then [x,<*y*>] in [:(product X),(product <*Y*>):] by A6, A1, FUNCT_2:5;

then A8: <*y*> in product <*Y*> by ZFMISC_1:87;

reconsider xx = x as Function by A5;

dom xx = dom X by CARD_3:9, A5

.= Seg (len X) by FINSEQ_1:def 3 ;

then reconsider x1 = xx as FinSequence by FINSEQ_1:def 2;

set y1 = <*y*>;

A9: J . (x,<*y*>) = x1 ^ <*y*> by A3, A5, A8;

J . (x,<*y*>) = K . (x,y) by A6, A7, FUNCT_2:15;

hence ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) by A9; :: thesis: verum