theorem :: MARGREL1:21

for n being Nat
for D being non empty set
for D1 being non empty Subset of D holds (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1