for X, Y being set
for F, G being Function of NAT,(bool X) st ( for i being Nat holds G . i = (F . i) /\ Y ) & Union F = Y holds
Union G = Union F