theorem :: HALLMAR1:25

for F being set
for A being FinSequence of bool F
for i being Element of NAT holds A is Reduction of A,i