theorem Th5: :: NDIFF_6:5

for X being non-empty non empty FinSequence
for Y being non empty set ex K being Function of [:(product X),Y:],(product (X ^ <*Y*>)) st
( K is bijective & ( for x being FinSequence
for y being object st x in product X & y in Y holds
K . (x,y) = x ^ <*y*> ) )