let X be non-empty non empty FinSequence; :: thesis:
let Y be non empty set ; :: thesis:
consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that
A1: ( I is bijective & ( for x, y being object st x in product X & y in Y holds
I . (x,y) = [x,<*y*>] ) ) by Th4;
consider J being Function of [:(product X),(product <*Y*>):],(product (X ^ <*Y*>)) such that
A2: ( J is one-to-one & J is onto & ( for x, y being FinSequence st x in product X & y in product <*Y*> 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:
A3: rng J = product (X ^ <*Y*>) by A2, FUNCT_2:def 3;
rng I = [:(product X),(product <*Y*>):] by A1, FUNCT_2:def 3;
then rng (J * I) = J .: [:(product X),(product <*Y*>):] by RELAT_1:127
.= product (X ^ <*Y*>) by A3, RELSET_1:22 ;
then K is onto by FUNCT_2:def 3;
hence K is bijective by A1, A2; :: thesis:
thus for x being FinSequence
for y being object st x in product X & y in Y holds
K . (x,y) = x ^ <*y*> :: thesis:

proof

let x be FinSequence; :: thesis:
let y be object ; :: thesis:
assume A4: ( x in product X & y in Y ) ; :: thesis:
then A5: I . (x,y) = [x,<*y*>] by A1;
[x,y] in [:(product X),Y:] by A4, ZFMISC_1:87;
then I . [x,y] in [:(product X),(product <*Y*>):] by FUNCT_2:5;
then <*y*> in product <*Y*> by A5, ZFMISC_1:87;
then J . (x,<*y*>) = x ^ <*y*> by A4, A2;
hence K . (x,y) = x ^ <*y*> by A5, A4, ZFMISC_1:87, FUNCT_2:15; :: thesis:

end;