theorem LM210: :: BINARI_6:32

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