theorem Th17: :: GROUP_14:17

for X being non-empty non empty FinSequence
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 ) ) )