:: deftheorem Def8 defines Singlification HALLMAR1:def 8 :
for F being non empty set
for A being FinSequence of bool F st A is non-empty holds
for b₃ being Reduction of A holds
( b₃ is Singlification of A iff for i being Element of NAT st i in dom A holds
card (b₃ . i) = 1 );