theorem Th1: :: FOMODEL0:1

for A, B being set
for m being Nat holds (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (m -tuples_on B)