:: deftheorem defines PartUnionNat PCOMPS_2:def 3 :
for X being set
for n being Element of NAT
for f being sequence of (bool X) holds PartUnionNat (n,f) = union (f .: ((Seg n) \ {n}));