theorem Th12: :: DIST_2:12

for S being non empty finite set
for s being FinSequence of S
for A being Subset of (dom s)
for f being Function st f = canFS A holds
(extract (s,A)) * (f ") = s | A