theorem Th6: :: FRIENDS1:6

for k, n being Nat
for X being non empty set
for A being non empty finite Subset of X
for P being Function of X,(bool X) st ( for x being object st x in X holds
card (P . x) = n ) holds
card { F where F is Element of (k + 1) -tuples_on X : ( F . 1 in A & ( for i being Nat st i in Seg k holds
F . (i + 1) in P . (F . i) ) ) } = (card A) * (n |^ k)