theorem :: FOMODEL0:22

for D being non empty set
for m, n being Nat holds (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):]