for F being non empty finite set
for A being non-empty non empty FinSequence of bool F
for f being Function holds
( f is Singlification of A iff ( dom f = dom A & ( for i being Element of NAT st i in dom A holds
f is Singlification of A,i ) ) )