theorem :: CLASSES4:113

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