:: Category of Rings
:: by Micha{\l} Muzalewski
::
:: Received December 5, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

::
:: 1a. Maps of the carriers of rings
::
definition
let G, H be non empty doubleLoopStr ;
let IT be Function of G,H;
attrIT is linear  means :Def1: :: RINGCAT1:def 1
( IT is additive & IT is multiplicative & IT is unity-preserving );
end;

:: deftheorem Def1 defines linear RINGCAT1:def_1_:_
 for G, H being non empty doubleLoopStr
for IT being Function of G,H holds
( IT is linear iff ( IT is additive & IT is multiplicative & IT is unity-preserving ) );

registration
let G, H be non empty doubleLoopStr ;
clusterV6() V28( the carrier of G, the carrier of H) linear  ->  unity-preserving multiplicative additive for Element of bool [: the carrier of G, the carrier of H:];
coherence
 for b1 being Function of G,H st b1 is linear holds
( b1 is additive & b1 is multiplicative & b1 is unity-preserving ) by Def1;
clusterV6() V28( the carrier of G, the carrier of H) unity-preserving multiplicative additive  ->  linear for Element of bool [: the carrier of G, the carrier of H:];
coherence
 for b1 being Function of G,H st b1 is additive & b1 is multiplicative & b1 is unity-preserving holds
b1 is linear by Def1;
end;

theorem Th1: :: RINGCAT1:1
for G1, G2, G3 being non empty doubleLoopStr
for f being Function of G1,G2
for g being Function of G2,G3 st f is linear & g is linear holds
g * f is linear
proofend;

::
:: 1b. Morphisms of rings
::
definition
attrc1 is strict ;
struct RingMorphismStr  -> ;
aggrRingMorphismStr(# Dom, Cod, Fun #) ->  RingMorphismStr ;
sel Dom c1 ->  Ring;
sel Cod c1 ->  Ring;
sel Fun c1 ->  Function of the Dom of c1, the Cod of c1;
end;

definition
let f be RingMorphismStr ;
func dom f ->  Ring equals :: RINGCAT1:def 2
 the Dom of f;
coherence
 the Dom of f is Ring ;
func cod f ->  Ring equals :: RINGCAT1:def 3
 the Cod of f;
coherence
 the Cod of f is Ring ;
func fun f ->  Function of the Dom of f, the Cod of f equals :: RINGCAT1:def 4
 the Fun of f;
coherence
 the Fun of f is Function of the Dom of f, the Cod of f ;
end;

:: deftheorem  defines dom RINGCAT1:def_2_:_
 for f being RingMorphismStr holds dom f = the Dom of f;

:: deftheorem  defines cod RINGCAT1:def_3_:_
 for f being RingMorphismStr holds cod f = the Cod of f;

:: deftheorem  defines fun RINGCAT1:def_4_:_
 for f being RingMorphismStr holds fun f = the Fun of f;

Lm1:  for G being non empty doubleLoopStr holds id G is linear
proofend;

registration
let G be non empty doubleLoopStr ;
cluster id G ->  linear ;
coherence
 id G is linear by Lm1;
end;

definition
let IT be RingMorphismStr ;
attrIT is RingMorphism-like  means :Def5: :: RINGCAT1:def 5
 fun IT is linear ;
end;

:: deftheorem Def5 defines RingMorphism-like RINGCAT1:def_5_:_
 for IT being RingMorphismStr holds
( IT is RingMorphism-like iff fun IT is linear );

registration
cluster strict RingMorphism-like for RingMorphismStr ;
existence
 ex b1 being RingMorphismStr st
( b1 is strict & b1 is RingMorphism-like )
proofend;
end;

definition
mode RingMorphism is RingMorphism-like RingMorphismStr ;
end;

definition
let G be Ring;
func ID G ->  RingMorphism equals :: RINGCAT1:def 6
 RingMorphismStr(# G,G,(id G) #);
coherence
 RingMorphismStr(# G,G,(id G) #) is RingMorphism
proofend;
end;

:: deftheorem  defines ID RINGCAT1:def_6_:_
 for G being Ring holds ID G = RingMorphismStr(# G,G,(id G) #);

registration
let G be Ring;
cluster ID G ->  strict ;
coherence
 ID G is strict ;
end;

definition
let G, H be Ring;
predG <= H means :Def7: :: RINGCAT1:def 7
 ex F being RingMorphism st
( dom F = G &amp; cod F = H );
reflexivity
 for G being Ring ex F being RingMorphism st
( dom F = G &amp; cod F = G )
proofend;
end;

:: deftheorem Def7 defines <= RINGCAT1:def_7_:_
 for G, H being Ring holds
( G <= H iff ex F being RingMorphism st
( dom F = G &amp; cod F = H ) );

Lm2:  for F being RingMorphism holds RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is RingMorphism-like
proofend;

definition
let G, H be Ring;
assume A1: G <= H ;
mode Morphism of G,H ->  strict RingMorphism means :Def8: :: RINGCAT1:def 8
( dom it = G &amp; cod it = H );
existence
 ex b1 being strict RingMorphism st
( dom b1 = G &amp; cod b1 = H )
proofend;
end;

:: deftheorem Def8 defines Morphism RINGCAT1:def_8_:_
 for G, H being Ring st G <= H holds
for b3 being strict RingMorphism holds
( b3 is Morphism of G,H iff ( dom b3 = G &amp; cod b3 = H ) );

registration
let G, H be Ring;
cluster strict RingMorphism-like for Morphism of G,H;
existence
 ex b1 being Morphism of G,H st b1 is strict
proofend;
end;

definition
let G be Ring;
:: original:ID
redefine func ID G ->  strict Morphism of G,G;
coherence
 ID G is strict Morphism of G,G
proofend;
end;

Lm3:  for F being RingMorphism holds the Fun of F is linear
proofend;

Lm4:  for G, H being Ring
for f being strict RingMorphismStr st dom f = G &amp; cod f = H &amp; fun f is linear holds
f is Morphism of G,H
proofend;

Lm5:  for G, H being Ring
for f being Function of G,H st f is linear holds
RingMorphismStr(# G,H,f #) is Morphism of G,H
proofend;

Lm6:  for F being RingMorphism ex G, H being Ring st
( G <= H &amp; dom F = G &amp; cod F = H &amp; RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is Morphism of G,H )
proofend;

theorem Th2: :: RINGCAT1:2
for g, f being RingMorphism st dom g = cod f holds
ex G1, G2, G3 being Ring st
( G1 <= G2 &amp; G2 <= G3 &amp; RingMorphismStr(# the Dom of g, the Cod of g, the Fun of g #) is Morphism of G2,G3 &amp; RingMorphismStr(# the Dom of f, the Cod of f, the Fun of f #) is Morphism of G1,G2 )
proofend;

theorem Th3: :: RINGCAT1:3
for F being strict RingMorphism holds
( F is Morphism of dom F, cod F &amp; dom F <= cod F )
proofend;

Lm7:  for G, H being Ring
for F being Morphism of G,H st G <= H holds
ex f being Function of G,H st
( F = RingMorphismStr(# G,H,f #) &amp; f is linear )
proofend;

Lm8:  for G, H being Ring
for F being Morphism of G,H st G <= H holds
ex f being Function of G,H st F = RingMorphismStr(# G,H,f #)
proofend;

theorem :: RINGCAT1:4
for F being strict RingMorphism ex G, H being Ring ex f being Function of G,H st
( F is Morphism of G,H &amp; F = RingMorphismStr(# G,H,f #) &amp; f is linear )
proofend;

definition
let G, F be RingMorphism;
assume A1: dom G = cod F ;
funcG * F ->  strict RingMorphism means :Def9: :: RINGCAT1:def 9
 for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) &amp; RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
it = RingMorphismStr(# G1,G3,(g * f) #);
existence
 ex b1 being strict RingMorphism st
for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) &amp; RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
b1 = RingMorphismStr(# G1,G3,(g * f) #)
proofend;
uniqueness
 for b1, b2 being strict RingMorphism st ( for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) &amp; RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
b1 = RingMorphismStr(# G1,G3,(g * f) #) ) &amp; ( for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) &amp; RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
b2 = RingMorphismStr(# G1,G3,(g * f) #) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines * RINGCAT1:def_9_:_
 for G, F being RingMorphism st dom G = cod F holds
for b3 being strict RingMorphism holds
( b3 = G * F iff for G1, G2, G3 being Ring
for g being Function of G2,G3
for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) &amp; RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
b3 = RingMorphismStr(# G1,G3,(g * f) #) );

theorem Th5: :: RINGCAT1:5
for G1, G2, G3 being Ring st G1 <= G2 &amp; G2 <= G3 holds
G1 <= G3
proofend;

theorem Th6: :: RINGCAT1:6
for G2, G3, G1 being Ring
for G being Morphism of G2,G3
for F being Morphism of G1,G2 st G1 <= G2 &amp; G2 <= G3 holds
G * F is Morphism of G1,G3
proofend;

definition
let G1, G2, G3 be Ring;
let G be Morphism of G2,G3;
let F be Morphism of G1,G2;
assume A1: ( G1 <= G2 &amp; G2 <= G3 ) ;
funcG *' F ->  strict Morphism of G1,G3 equals :Def10: :: RINGCAT1:def 10
G * F;
coherence
 G * F is strict Morphism of G1,G3 by A1, Th6;
end;

:: deftheorem Def10 defines *' RINGCAT1:def_10_:_
 for G1, G2, G3 being Ring
for G being Morphism of G2,G3
for F being Morphism of G1,G2 st G1 <= G2 &amp; G2 <= G3 holds
G *' F = G * F;

theorem Th7: :: RINGCAT1:7
for f, g being strict RingMorphism st dom g = cod f holds
ex G1, G2, G3 being Ring ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = RingMorphismStr(# G1,G2,f0 #) &amp; g = RingMorphismStr(# G2,G3,g0 #) &amp; g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) )
proofend;

theorem Th8: :: RINGCAT1:8
for f, g being strict RingMorphism st dom g = cod f holds
( dom (g * f) = dom f &amp; cod (g * f) = cod g )
proofend;

theorem Th9: :: RINGCAT1:9
for G1, G2, G3, G4 being Ring
for f being Morphism of G1,G2
for g being Morphism of G2,G3
for h being Morphism of G3,G4 st G1 <= G2 &amp; G2 <= G3 &amp; G3 <= G4 holds
h * (g * f) = (h * g) * f
proofend;

theorem Th10: :: RINGCAT1:10
for f, g, h being strict RingMorphism st dom h = cod g &amp; dom g = cod f holds
h * (g * f) = (h * g) * f
proofend;

theorem :: RINGCAT1:11
for G being Ring holds
( dom (ID G) = G &amp; cod (ID G) = G &amp; ( for f being strict RingMorphism st cod f = G holds
(ID G) * f = f ) &amp; ( for g being strict RingMorphism st dom g = G holds
g * (ID G) = g ) )
proofend;

::
:: 2. Domains of rings
::
definition
let IT be set ;
attrIT is Ring_DOMAIN-like  means :Def11: :: RINGCAT1:def 11
 for x being Element of IT holds x is strict Ring;
end;

:: deftheorem Def11 defines Ring_DOMAIN-like RINGCAT1:def_11_:_
 for IT being set holds
( IT is Ring_DOMAIN-like iff for x being Element of IT holds x is strict Ring );

registration
cluster non empty Ring_DOMAIN-like for set ;
existence
 ex b1 being set st
( b1 is Ring_DOMAIN-like &amp; not b1 is empty )
proofend;
end;

definition
mode Ring_DOMAIN is non empty Ring_DOMAIN-like set ;
end;

definition
let V be Ring_DOMAIN;
:: original:Element
redefine mode Element of V ->  Ring;
coherence
 for b1 being Element of V holds b1 is Ring by Def11;
end;

registration
let V be Ring_DOMAIN;
cluster non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital for Element of V;
existence
 ex b1 being Element of V st b1 is strict
proofend;
end;

definition
let IT be set ;
attrIT is RingMorphism_DOMAIN-like  means :Def12: :: RINGCAT1:def 12
 for x being set st x in IT holds
x is strict RingMorphism;
end;

:: deftheorem Def12 defines RingMorphism_DOMAIN-like RINGCAT1:def_12_:_
 for IT being set holds
( IT is RingMorphism_DOMAIN-like iff for x being set st x in IT holds
x is strict RingMorphism );

registration
cluster non empty RingMorphism_DOMAIN-like for set ;
existence
 ex b1 being non empty set st b1 is RingMorphism_DOMAIN-like
proofend;
end;

definition
mode RingMorphism_DOMAIN is non empty RingMorphism_DOMAIN-like set ;
end;

definition
let M be RingMorphism_DOMAIN;
:: original:Element
redefine mode Element of M ->  RingMorphism;
coherence
 for b1 being Element of M holds b1 is RingMorphism by Def12;
end;

registration
let M be RingMorphism_DOMAIN;
cluster strict RingMorphism-like for Element of M;
existence
 ex b1 being Element of M st b1 is strict
proofend;
end;

theorem Th12: :: RINGCAT1:12
for f being strict RingMorphism holds {f} is RingMorphism_DOMAIN
proofend;

definition
let G, H be Ring;
mode RingMorphism_DOMAIN of G,H ->  RingMorphism_DOMAIN means :Def13: :: RINGCAT1:def 13
 for x being Element of it holds x is Morphism of G,H;
existence
 ex b1 being RingMorphism_DOMAIN st
for x being Element of b1 holds x is Morphism of G,H
proofend;
end;

:: deftheorem Def13 defines RingMorphism_DOMAIN RINGCAT1:def_13_:_
 for G, H being Ring
for b3 being RingMorphism_DOMAIN holds
( b3 is RingMorphism_DOMAIN of G,H iff for x being Element of b3 holds x is Morphism of G,H );

theorem Th13: :: RINGCAT1:13
for D being non empty set
for G, H being Ring holds
( D is RingMorphism_DOMAIN of G,H iff for x being Element of D holds x is Morphism of G,H )
proofend;

theorem :: RINGCAT1:14
for G, H being Ring
for f being Morphism of G,H holds {f} is RingMorphism_DOMAIN of G,H
proofend;

definition
let G, H be Ring;
assume A1: G <= H ;
func Morphs (G,H) ->  RingMorphism_DOMAIN of G,H means :Def14: :: RINGCAT1:def 14
 for x being set holds
( x in it iff x is Morphism of G,H );
existence
 ex b1 being RingMorphism_DOMAIN of G,H st
for x being set holds
( x in b1 iff x is Morphism of G,H )
proofend;
uniqueness
 for b1, b2 being RingMorphism_DOMAIN of G,H st ( for x being set holds
( x in b1 iff x is Morphism of G,H ) ) &amp; ( for x being set holds
( x in b2 iff x is Morphism of G,H ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines Morphs RINGCAT1:def_14_:_
 for G, H being Ring st G <= H holds
for b3 being RingMorphism_DOMAIN of G,H holds
( b3 = Morphs (G,H) iff for x being set holds
( x in b3 iff x is Morphism of G,H ) );

definition
let G, H be Ring;
let M be RingMorphism_DOMAIN of G,H;
:: original:Element
redefine mode Element of M ->  Morphism of G,H;
coherence
 for b1 being Element of M holds b1 is Morphism of G,H by Def13;
end;

registration
let G, H be Ring;
let M be RingMorphism_DOMAIN of G,H;
cluster strict RingMorphism-like for Element of M;
existence
 ex b1 being Element of M st b1 is strict
proofend;
end;

::
:: 4a. Category of rings - objects
::
definition
let x, y be set ;
pred GO x,y means :Def15: :: RINGCAT1:def 15
 ex x1, x2, x3, x4, x5, x6 being set st
( x = [[x1,x2,x3,x4],x5,x6] &amp; ex G being strict Ring st
( y = G &amp; x1 = the carrier of G &amp; x2 = the addF of G &amp; x3 = comp G &amp; x4 = 0. G &amp; x5 = the multF of G &amp; x6 = 1. G ) );
end;

:: deftheorem Def15 defines GO RINGCAT1:def_15_:_
 for x, y being set holds
( GO x,y iff ex x1, x2, x3, x4, x5, x6 being set st
( x = [[x1,x2,x3,x4],x5,x6] &amp; ex G being strict Ring st
( y = G &amp; x1 = the carrier of G &amp; x2 = the addF of G &amp; x3 = comp G &amp; x4 = 0. G &amp; x5 = the multF of G &amp; x6 = 1. G ) ) );

theorem Th15: :: RINGCAT1:15
for x, y1, y2 being set st GO x,y1 &amp; GO x,y2 holds
y1 = y2
proofend;

theorem Th16: :: RINGCAT1:16
for UN being Universe ex x being set st
( x in UN &amp; GO x, Z_3 )
proofend;

definition
let UN be Universe;
func RingObjects UN ->  set  means :Def16: :: RINGCAT1:def 16
 for y being set holds
( y in it iff ex x being set st
( x in UN &amp; GO x,y ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ex x being set st
( x in UN &amp; GO x,y ) )
proofend;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st
( x in UN &amp; GO x,y ) ) ) &amp; ( for y being set holds
( y in b2 iff ex x being set st
( x in UN &amp; GO x,y ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines RingObjects RINGCAT1:def_16_:_
 for UN being Universe
for b2 being set holds
( b2 = RingObjects UN iff for y being set holds
( y in b2 iff ex x being set st
( x in UN &amp; GO x,y ) ) );

theorem Th17: :: RINGCAT1:17
for UN being Universe holds Z_3 in RingObjects UN
proofend;

registration
let UN be Universe;
cluster RingObjects UN ->  non empty ;
coherence
 not RingObjects UN is empty by Th17;
end;

theorem Th18: :: RINGCAT1:18
for UN being Universe
for x being Element of RingObjects UN holds x is strict Ring
proofend;

registration
let UN be Universe;
cluster RingObjects UN ->  Ring_DOMAIN-like ;
coherence
 RingObjects UN is Ring_DOMAIN-like
proofend;
end;

::
:: 4b. Category of rings - morphisms
::
definition
let V be Ring_DOMAIN;
func Morphs V ->  RingMorphism_DOMAIN means :Def17: :: RINGCAT1:def 17
 for x being set holds
( x in it iff ex G, H being Element of V st
( G <= H &amp; x is Morphism of G,H ) );
existence
 ex b1 being RingMorphism_DOMAIN st
for x being set holds
( x in b1 iff ex G, H being Element of V st
( G <= H &amp; x is Morphism of G,H ) )
proofend;
uniqueness
 for b1, b2 being RingMorphism_DOMAIN st ( for x being set holds
( x in b1 iff ex G, H being Element of V st
( G <= H &amp; x is Morphism of G,H ) ) ) &amp; ( for x being set holds
( x in b2 iff ex G, H being Element of V st
( G <= H &amp; x is Morphism of G,H ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines Morphs RINGCAT1:def_17_:_
 for V being Ring_DOMAIN
for b2 being RingMorphism_DOMAIN holds
( b2 = Morphs V iff for x being set holds
( x in b2 iff ex G, H being Element of V st
( G <= H &amp; x is Morphism of G,H ) ) );

::
:: 4c. Category of rings - dom,cod,id
::
definition
let V be Ring_DOMAIN;
let F be Element of Morphs V;
:: original:dom
redefine func dom F ->  Element of V;
coherence
 dom F is Element of V
proofend;
:: original:cod
redefine func cod F ->  Element of V;
coherence
 cod F is Element of V
proofend;
end;

definition
let V be Ring_DOMAIN;
let G be Element of V;
func ID G ->  strict Element of Morphs V equals :: RINGCAT1:def 18
 ID G;
coherence
 ID G is strict Element of Morphs V by Def17;
canceled;
end;

:: deftheorem  defines ID RINGCAT1:def_18_:_
 for V being Ring_DOMAIN
for G being Element of V holds ID G = ID G;

:: deftheorem  RINGCAT1:def_19_:_
canceled;

definition
let V be Ring_DOMAIN;
func dom V ->  Function of (Morphs V),V means :Def19: :: RINGCAT1:def 20
 for f being Element of Morphs V holds it . f = dom f;
existence
 ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = dom f
proofend;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = dom f ) &amp; ( for f being Element of Morphs V holds b2 . f = dom f ) holds
b1 = b2
proofend;
func cod V ->  Function of (Morphs V),V means :Def20: :: RINGCAT1:def 21
 for f being Element of Morphs V holds it . f = cod f;
existence
 ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = cod f
proofend;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = cod f ) &amp; ( for f being Element of Morphs V holds b2 . f = cod f ) holds
b1 = b2
proofend;
canceled;
end;

:: deftheorem Def19 defines dom RINGCAT1:def_20_:_
 for V being Ring_DOMAIN
for b2 being Function of (Morphs V),V holds
( b2 = dom V iff for f being Element of Morphs V holds b2 . f = dom f );

:: deftheorem Def20 defines cod RINGCAT1:def_21_:_
 for V being Ring_DOMAIN
for b2 being Function of (Morphs V),V holds
( b2 = cod V iff for f being Element of Morphs V holds b2 . f = cod f );

:: deftheorem  RINGCAT1:def_22_:_
canceled;

::
:: 4d. Category of rings - superposition
::
theorem Th19: :: RINGCAT1:19
for V being Ring_DOMAIN
for g, f being Element of Morphs V st dom g = cod f holds
ex G1, G2, G3 being Element of V st
( G1 <= G2 &amp; G2 <= G3 &amp; g is Morphism of G2,G3 &amp; f is Morphism of G1,G2 )
proofend;

theorem Th20: :: RINGCAT1:20
for V being Ring_DOMAIN
for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
proofend;

definition
let V be Ring_DOMAIN;
func comp V ->  PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) means :Def22: :: RINGCAT1:def 23
( ( for g, f being Element of Morphs V holds
( [g,f] in dom it iff dom g = cod f ) ) &amp; ( for g, f being Element of Morphs V st [g,f] in dom it holds
it . (g,f) = g * f ) );
existence
 ex b1 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st
( ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom g = cod f ) ) &amp; ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom g = cod f ) ) &amp; ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) &amp; ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom g = cod f ) ) &amp; ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . (g,f) = g * f ) holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines comp RINGCAT1:def_23_:_
 for V being Ring_DOMAIN
for b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds
( b2 = comp V iff ( ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom g = cod f ) ) &amp; ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . (g,f) = g * f ) ) );

::
:: 4e. Definition of Category of rings
::
definition
let UN be Universe;
func RingCat UN ->  CatStr  equals :: RINGCAT1:def 24
 CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)) #);
coherence
 CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)) #) is CatStr ;
end;

:: deftheorem  defines RingCat RINGCAT1:def_24_:_
 for UN being Universe holds RingCat UN = CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)) #);

registration
let UN be Universe;
cluster RingCat UN ->  non empty non void strict ;
coherence
 ( RingCat UN is strict &amp; not RingCat UN is void &amp; not RingCat UN is empty ) ;
end;

theorem Th21: :: RINGCAT1:21
for UN being Universe
for f, g being Morphism of (RingCat UN) holds
( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f )
proofend;

theorem Th22: :: RINGCAT1:22
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) &amp; f9 is Morphism of (RingCat UN) &amp; b is strict Element of RingObjects UN &amp; b9 is Object of (RingCat UN) )
proofend;

theorem :: RINGCAT1:23
canceled;

theorem Th24: :: RINGCAT1:24
for UN being Universe
for f, g being Morphism of (RingCat UN)
for f9, g9 being Element of Morphs (RingObjects UN) st f = f9 &amp; g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) &amp; ( dom g9 = cod f9 implies dom g = cod f ) &amp; ( dom g = cod f implies [g9,f9] in dom (comp (RingObjects UN)) ) &amp; ( [g9,f9] in dom (comp (RingObjects UN)) implies dom g = cod f ) &amp; ( dom g = cod f implies g (*) f = g9 * f9 ) &amp; ( dom f = dom g implies dom f9 = dom g9 ) &amp; ( dom f9 = dom g9 implies dom f = dom g ) &amp; ( cod f = cod g implies cod f9 = cod g9 ) &amp; ( cod f9 = cod g9 implies cod f = cod g ) )
proofend;

Lm9:  for UN being Universe
for f, g being Morphism of (RingCat UN) st dom g = cod f holds
( dom (g (*) f) = dom f &amp; cod (g (*) f) = cod g )
proofend;

Lm10:  for UN being Universe
for f, g, h being Morphism of (RingCat UN) st dom h = cod g &amp; dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
proofend;

registration
let UN be Universe;
cluster RingCat UN ->  Category-like transitive associative reflexive ;
coherence
 ( RingCat UN is Category-like &amp; RingCat UN is transitive &amp; RingCat UN is associative &amp; RingCat UN is reflexive )
proofend;
end;

LmX:  for UN being Universe
for a being Element of (RingCat UN)
for aa being Element of RingObjects UN st a = aa holds
for i being Morphism of a,a st i = ID aa holds
for b being Element of (RingCat UN) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) &amp; ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
proofend;

registration
let UN be Universe;
cluster RingCat UN ->  with_identities ;
coherence
 RingCat UN is with_identities
proofend;
end;

theorem :: RINGCAT1:25
for UN being Universe
for a being Object of (RingCat UN)
for aa being Element of RingObjects UN st a = aa holds
id a = ID aa
proofend;