theorem Th23: :: DIST_2:23

for S being non empty finite set
for s being Element of S *
for f being Function of S,BOOLEAN holds Coim ((('not' f) * s),TRUE) = (dom s) \ (Coim ((f * s),TRUE))