let UN be 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) )
set C = RingCat UN;
set V = RingObjects UN;
set X = Morphs (RingObjects UN);
let f be 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) )
let f9 be 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) )
let b be 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) )
let b9 be Element of RingObjects UN; ( 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) )
consider x being set such that
x in UN
and
A1:
GO x,b
by Def16;
ex G, H being Element of RingObjects UN st
( G <= H & f is Morphism of G,H )
by Def17;
hence
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) )
thus
f9 is Morphism of (RingCat UN)
; ( b is strict Element of RingObjects UN & b9 is Object of (RingCat UN) )
ex x1, x2, x3, x4, x5, x6 being set st
( x = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( b = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) )
by A1;
hence
b is strict Element of RingObjects UN
; b9 is Object of (RingCat UN)
thus
b9 is Object of (RingCat UN)
; verum