theorem Th2: :: CIRCCOMB:2

for X being set
for Y being non empty set
for p being FinSequence of X holds ((X --> Y) #) . p = (len p) -tuples_on Y