for X being with_empty_element set
for F being FinSequence of X ex G being Function of NAT,X st
( ( for i being Nat holds F . i = G . i ) & Union F = Union G )