for x being object
for X being set
for F1 being FinSequence of bool X holds
( x in Union F1 iff ex k being Nat st
( k in dom F1 & x in F1 . k ) )