:: deftheorem Def5 defines Reduction HALLMAR1:def 5 :
for F being set
for A being FinSequence of bool F
for i being Element of NAT
for b₄ being FinSequence of bool F holds
( b₄ is Reduction of A,i iff ( dom b₄ = dom A & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = b₄ . j ) & b₄ . i c= A . i ) );