theorem Th21: :: DIST_2:21

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