theorem :: CLASSES4:111

ex f being Function of NAT,(union (union (rng sequence_univers))) st
for i being Nat holds f . i in ComplUniverse . i