for UN being Universe
for f being Morphism of (RingCat UN)
for f9 being Element of Morphs (RingObjects UN)
for b being Object of (RingCat UN)
for b9 being Element of RingObjects UN holds
( f is strict Element of Morphs (RingObjects UN) & f9 is Morphism of (RingCat UN) & b is strict Element of RingObjects UN & b9 is Object of (RingCat UN) )