ex F being Function of (BOOLEAN *),NAT st
for x being Element of BOOLEAN * ex x0 being Tuple of len x, BOOLEAN st
( x = x0 & F . x = Absval x0 )