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*> <> {}
proof
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;
consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that
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
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 reconsider YY = <*Y*> as non-empty non empty FinSequence ;
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;