let UN be Universe; :: thesis: for f being Morphism of
for f' being Element of Morphs (RingObjects UN)
for b being Object of
for b' being Element of RingObjects UN holds
( f is strict Element of Morphs (RingObjects UN) & f' is Morphism of & b is strict Element of RingObjects UN & b' is Object of )
set C = RingCat UN;
set V = RingObjects UN;
set X = Morphs (RingObjects UN);
let f be Morphism of ; :: thesis: for f' being Element of Morphs (RingObjects UN)
for b being Object of
for b' being Element of RingObjects UN holds
( f is strict Element of Morphs (RingObjects UN) & f' is Morphism of & b is strict Element of RingObjects UN & b' is Object of )
let f' be Element of Morphs (RingObjects UN); :: thesis: for b being Object of
for b' being Element of RingObjects UN holds
( f is strict Element of Morphs (RingObjects UN) & f' is Morphism of & b is strict Element of RingObjects UN & b' is Object of )
let b be Object of ; :: thesis: for b' being Element of RingObjects UN holds
( f is strict Element of Morphs (RingObjects UN) & f' is Morphism of & b is strict Element of RingObjects UN & b' is Object of )
let b' be Element of RingObjects UN; :: thesis: ( f is strict Element of Morphs (RingObjects UN) & f' is Morphism of & b is strict Element of RingObjects UN & b' is Object of )
consider x being set such that
x in UN and
A1: GO x,b by Def17;
ex G, H being Element of RingObjects UN st
( G <= H & f is Morphism of G,H ) by Def18;
hence f is strict Element of Morphs (RingObjects UN) ; :: thesis: ( f' is Morphism of & b is strict Element of RingObjects UN & b' is Object of )
thus f' is Morphism of ; :: thesis: ( b is strict Element of RingObjects UN & b' is Object of )
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, Def16;
hence b is strict Element of RingObjects UN ; :: thesis: b' is Object of
thus b' is Object of ; :: thesis: verum