theorem :: CLASSES4:112

for f being Function of NAT,(union (rng sequence_univers)) holds f in super_univers