theorem Th11: :: DIST_2:11

for S being set
for s being FinSequence of S
for A being Subset of (dom s) holds
( len (extract (s,A)) = card A & ( for i being Nat st i in dom (extract (s,A)) holds
(extract (s,A)) . i = s . ((canFS A) . i) ) )