theorem Th6: :: PRVECT_3:6

for X, Y being non-empty non empty FinSequence ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st
( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product X & y in product Y holds
I . (x,y) = x ^ y ) )