theorem Th44: :: STIRL2_1:44

for f being Function
for n being Nat holds (union (rng (f | n))) \/ (f . n) = union (rng (f | (n + 1)))