ex F being Function of (BOOLEAN *),NAT st
for x being Element of BOOLEAN * holds F . x = ExAbsval x