theorem Th7: :: HALLMAR1:7

for J being set
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT st i in J & i in dom A holds
A . i c= union (A,J) by Def1;