theorem Th35: :: DIST_2:35

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 set st SD = s " X & t = extract (s,SD) & x in X holds
frequency (x,s) = frequency (x,t)