:: deftheorem Def7 defines Singlification HALLMAR1:def 7 :
for F being set
for A being FinSequence of bool F
for i being Nat st i in dom A & A . i <> {} holds
for b₄ being Reduction of A holds
( b₄ is Singlification of A,i iff card (b₄ . i) = 1 );