theorem Th2: :: FOMODEL0:2

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