theorem Th12: :: HALLMAR1:12

for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i}))