:: deftheorem defines extract DIST_2:def 5 :
for S being set
for s being FinSequence of S
for A being Subset of (dom s) holds extract (s,A) = s * (canFS A);