theorem Th22: :: DIST_2:22

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