theorem Th34: :: DIST_2:34

for S being non empty finite set
for X being Subset of S
for s, t being FinSequence of S
for SD being Subset of (dom s)
for x being Subset of X st SD = s " X & t = extract (s,SD) holds
card (s " x) = card (t " x)