:: RINGCAT1 semantic presentation

begin


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
proof
let G1, G2, G3 be non empty doubleLoopStr ; ::_thesis: 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
let f be Function of G1,G2; ::_thesis: for g being Function of G2,G3 st f is linear & g is linear holds
g * f is linear
let g be Function of G2,G3; ::_thesis: ( f is linear & g is linear implies g * f is linear )
assume that
A1: ( f is additive & f is multiplicative & f is unity-preserving ) and
A2: ( g is additive & g is multiplicative & g is unity-preserving ) ; :: according to RINGCAT1:def_1 ::_thesis: g * f is linear
set h = g * f;
thus  g * f is additive :: according to RINGCAT1:def_1 ::_thesis: ( g * f is multiplicative & g * f is unity-preserving )
proof
let x, y be Scalar of G1; :: according to VECTSP_1:def_20 ::_thesis: (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)
A3: ( g . (f . x) = (g * f) . x & g . (f . y) = (g * f) . y ) by FUNCT_2:15;
thus (g * f) . (x + y) = g . (f . (x + y)) by FUNCT_2:15
.= g . ((f . x) + (f . y)) by A1, VECTSP_1:def_20
.= ((g * f) . x) + ((g * f) . y) by A2, A3, VECTSP_1:def_20 ; ::_thesis: verum
end;
thus  g * f is multiplicative ::_thesis: g * f is unity-preserving
proof
let x, y be Scalar of G1; :: according to GROUP_6:def_6 ::_thesis: (g * f) . (x * y) = ((g * f) . x) * ((g * f) . y)
A4: ( g . (f . x) = (g * f) . x & g . (f . y) = (g * f) . y ) by FUNCT_2:15;
thus (g * f) . (x * y) = g . (f . (x * y)) by FUNCT_2:15
.= g . ((f . x) * (f . y)) by A1, GROUP_6:def_6
.= ((g * f) . x) * ((g * f) . y) by A2, A4, GROUP_6:def_6 ; ::_thesis: verum
end;
thus (g * f) . (1_ G1) = g . (f . (1_ G1)) by FUNCT_2:15
.= g . (1_ G2) by A1, GROUP_1:def_13
.= 1_ G3 by A2, GROUP_1:def_13 ; :: according to GROUP_1:def_13 ::_thesis: verum
end;

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
proof
let G be non empty doubleLoopStr ; ::_thesis: id G is linear
set f = id G;
thus  id G is additive ; :: according to RINGCAT1:def_1 ::_thesis: ( id G is multiplicative & id G is unity-preserving )
thus  id G is multiplicative ::_thesis: id G is unity-preserving
proof
let x, y be Scalar of G; :: according to GROUP_6:def_6 ::_thesis: (id G) . (x * y) = ((id G) . x) * ((id G) . y)
 ( (id G) . (x * y) = x * y & (id G) . x = x ) by FUNCT_1:18;
hence  (id G) . (x * y) = ((id G) . x) * ((id G) . y) by FUNCT_1:18; ::_thesis: verum
end;
thus  (id G) . (1_ G) = 1_ G by FUNCT_1:18; :: according to GROUP_1:def_13 ::_thesis: verum
end;

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 )
proof
set G = the Ring;
set i = RingMorphismStr(# the Ring, the Ring,(id the Ring) #);
 fun RingMorphismStr(# the Ring, the Ring,(id the Ring) #) = id the Ring ;
hence  ex b1 being RingMorphismStr st
( b1 is strict & b1 is RingMorphism-like ) by Def5; ::_thesis: verum
end;
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
proof
set i = RingMorphismStr(# G,G,(id G) #);
 fun RingMorphismStr(# G,G,(id G) #) = id G ;
hence  RingMorphismStr(# G,G,(id G) #) is RingMorphism by Def5; ::_thesis: verum
end;
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 & cod F = H );
reflexivity
 for G being Ring ex F being RingMorphism st
( dom F = G & cod F = G )
proof
let G be Ring; ::_thesis: ex F being RingMorphism st
( dom F = G & cod F = G )
set i = ID G;
take  ID G ; ::_thesis: ( dom (ID G) = G & cod (ID G) = G )
thus  ( dom (ID G) = G & cod (ID G) = G ) ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines <= RINGCAT1:def_7_:_
 for G, H being Ring holds
( G <= H iff ex F being RingMorphism st
( dom F = G & 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
proof
let F be RingMorphism; ::_thesis: RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is RingMorphism-like
set S = RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #);
A1: fun F is linear by Def5;
hence  for x, y being Scalar of the Dom of RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) holds (fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . (x + y) = ((fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . x) + ((fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . y) by VECTSP_1:def_20; :: according to VECTSP_1:def_20,RINGCAT1:def_1,RINGCAT1:def_5 ::_thesis: ( fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is multiplicative & fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is unity-preserving )
thus  for x, y being Scalar of the Dom of RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) holds (fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . (x * y) = ((fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . x) * ((fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #)) . y) by A1, GROUP_6:def_6; :: according to GROUP_6:def_6 ::_thesis: fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is unity-preserving
thus  fun RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is unity-preserving by A1; ::_thesis: verum
end;

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 & cod it = H );
existence
 ex b1 being strict RingMorphism st
( dom b1 = G & cod b1 = H )
proof
consider F being RingMorphism such that
A2: ( dom F = G & cod F = H ) by A1, Def7;
set S = RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #);
A3: ( dom RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = G & cod RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = H ) by A2;
 RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is RingMorphism by Lm2;
hence  ex b1 being strict RingMorphism st
( dom b1 = G & cod b1 = H ) by A3; ::_thesis: verum
end;
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 & 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
proof
set m = the Morphism of G,H;
 the Morphism of G,H is RingMorphism ;
hence  ex b1 being Morphism of G,H st b1 is strict ; ::_thesis: verum
end;
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
proof
set i = ID G;
 ( dom (ID G) = G & cod (ID G) = G ) ;
hence  ID G is strict Morphism of G,G by Def8; ::_thesis: verum
end;
end;

Lm3:  for F being RingMorphism holds the Fun of F is linear
proof
let F be RingMorphism; ::_thesis: the Fun of F is linear
 the Fun of F = fun F ;
hence  the Fun of F is linear by Def5; ::_thesis: verum
end;

Lm4:  for G, H being Ring
for f being strict RingMorphismStr st dom f = G & cod f = H & fun f is linear holds
f is Morphism of G,H
proof
let G, H be Ring; ::_thesis: for f being strict RingMorphismStr st dom f = G & cod f = H & fun f is linear holds
f is Morphism of G,H
let f be strict RingMorphismStr ; ::_thesis: ( dom f = G & cod f = H & fun f is linear implies f is Morphism of G,H )
assume that
A1: dom f = G and
A2: cod f = H and
A3: fun f is linear ; ::_thesis: f is Morphism of G,H
reconsider f9 = f as RingMorphism by A3, Def5;
 dom f9 = G by A1;
then  G <= H by A2, Def7;
then  f9 is Morphism of G,H by A1, A2, Def8;
hence  f is Morphism of G,H ; ::_thesis: verum
end;

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
proof
let G, H be Ring; ::_thesis: for f being Function of G,H st f is linear holds
RingMorphismStr(# G,H,f #) is Morphism of G,H
let f be Function of G,H; ::_thesis: ( f is linear implies RingMorphismStr(# G,H,f #) is Morphism of G,H )
assume A1: f is linear ; ::_thesis: RingMorphismStr(# G,H,f #) is Morphism of G,H
set F = RingMorphismStr(# G,H,f #);
A2: fun RingMorphismStr(# G,H,f #) = f ;
 ( dom RingMorphismStr(# G,H,f #) = G & cod RingMorphismStr(# G,H,f #) = H ) ;
hence  RingMorphismStr(# G,H,f #) is Morphism of G,H by A1, A2, Lm4; ::_thesis: verum
end;

Lm6:  for F being RingMorphism ex G, H being Ring st
( G <= H & dom F = G & cod F = H & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is Morphism of G,H )
proof
let F be RingMorphism; ::_thesis: ex G, H being Ring st
( G <= H & dom F = G & cod F = H & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is Morphism of G,H )
reconsider S = RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) as RingMorphism by Lm2;
set G = the Dom of F;
set H = the Cod of F;
take  the Dom of F ; ::_thesis: ex H being Ring st
( the Dom of F <= H & dom F = the Dom of F & cod F = H & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is Morphism of the Dom of F,H )
take  the Cod of F ; ::_thesis: ( the Dom of F <= the Cod of F & dom F = the Dom of F & cod F = the Cod of F & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is Morphism of the Dom of F, the Cod of F )
 ( dom F = the Dom of F & cod F = the Cod of F ) ;
then A1: the Dom of F <= the Cod of F by Def7;
 ( dom S = the Dom of F & cod S = the Cod of F ) ;
hence  ( the Dom of F <= the Cod of F & dom F = the Dom of F & cod F = the Cod of F & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is Morphism of the Dom of F, the Cod of F ) by A1, Def8; ::_thesis: verum
end;

theorem Th2: :: RINGCAT1:2
for g, f being RingMorphism st dom g = cod f holds
ex G1, G2, G3 being Ring st
( G1 <= G2 & G2 <= G3 & RingMorphismStr(# the Dom of g, the Cod of g, the Fun of g #) is Morphism of G2,G3 & RingMorphismStr(# the Dom of f, the Cod of f, the Fun of f #) is Morphism of G1,G2 )
proof
defpred S1[ RingMorphism, RingMorphism] means  dom $1 = cod $2;
let g, f be RingMorphism; ::_thesis: ( dom g = cod f implies ex G1, G2, G3 being Ring st
( G1 <= G2 & G2 <= G3 & RingMorphismStr(# the Dom of g, the Cod of g, the Fun of g #) is Morphism of G2,G3 & RingMorphismStr(# the Dom of f, the Cod of f, the Fun of f #) is Morphism of G1,G2 ) )
assume A1: S1[g,f] ; ::_thesis: ex G1, G2, G3 being Ring st
( G1 <= G2 & G2 <= G3 & RingMorphismStr(# the Dom of g, the Cod of g, the Fun of g #) is Morphism of G2,G3 & RingMorphismStr(# the Dom of f, the Cod of f, the Fun of f #) is Morphism of G1,G2 )
 ( ex G2, G3 being Ring st
( G2 <= G3 & dom g = G2 & cod g = G3 & RingMorphismStr(# the Dom of g, the Cod of g, the Fun of g #) is Morphism of G2,G3 ) & ex G1, G29 being Ring st
( G1 <= G29 & dom f = G1 & cod f = G29 & RingMorphismStr(# the Dom of f, the Cod of f, the Fun of f #) is Morphism of G1,G29 ) ) by Lm6;
hence  ex G1, G2, G3 being Ring st
( G1 <= G2 & G2 <= G3 & RingMorphismStr(# the Dom of g, the Cod of g, the Fun of g #) is Morphism of G2,G3 & RingMorphismStr(# the Dom of f, the Cod of f, the Fun of f #) is Morphism of G1,G2 ) by A1; ::_thesis: verum
end;

theorem Th3: :: RINGCAT1:3
for F being strict RingMorphism holds
( F is Morphism of dom F, cod F & dom F <= cod F )
proof
let F be strict RingMorphism; ::_thesis: ( F is Morphism of dom F, cod F & dom F <= cod F )
 ex G, H being Ring st
( G <= H & dom F = G & cod F = H & F is Morphism of G,H ) by Lm6;
hence  ( F is Morphism of dom F, cod F & dom F <= cod F ) ; ::_thesis: verum
end;

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 #) & f is linear )
proof
let G, H be Ring; ::_thesis: for F being Morphism of G,H st G <= H holds
ex f being Function of G,H st
( F = RingMorphismStr(# G,H,f #) & f is linear )
let F be Morphism of G,H; ::_thesis: ( G <= H implies ex f being Function of G,H st
( F = RingMorphismStr(# G,H,f #) & f is linear ) )
assume A1: G <= H ; ::_thesis: ex f being Function of G,H st
( F = RingMorphismStr(# G,H,f #) & f is linear )
A2: the Cod of F = cod F
.= H by A1, Def8 ;
A3: the Dom of F = dom F
.= G by A1, Def8 ;
then reconsider f = the Fun of F as Function of G,H by A2;
take  f ; ::_thesis: ( F = RingMorphismStr(# G,H,f #) & f is linear )
thus  ( F = RingMorphismStr(# G,H,f #) & f is linear ) by A3, A2, Lm3; ::_thesis: verum
end;

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 #)
proof
let G, H be Ring; ::_thesis: for F being Morphism of G,H st G <= H holds
ex f being Function of G,H st F = RingMorphismStr(# G,H,f #)
let F be Morphism of G,H; ::_thesis: ( G <= H implies ex f being Function of G,H st F = RingMorphismStr(# G,H,f #) )
assume  G <= H ; ::_thesis: ex f being Function of G,H st F = RingMorphismStr(# G,H,f #)
then consider f being Function of G,H such that
A1: F = RingMorphismStr(# G,H,f #) and
 f is linear by Lm7;
take  f ; ::_thesis: F = RingMorphismStr(# G,H,f #)
thus  F = RingMorphismStr(# G,H,f #) by A1; ::_thesis: verum
end;

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 & F = RingMorphismStr(# G,H,f #) & f is linear )
proof
let F be strict RingMorphism; ::_thesis: ex G, H being Ring ex f being Function of G,H st
( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
consider G, H being Ring such that
A1: G <= H and
 dom F = G and
 cod F = H and
A2: F is Morphism of G,H by Lm6;
reconsider F9 = F as Morphism of G,H by A2;
consider f being Function of G,H such that
A3: ( F9 = RingMorphismStr(# G,H,f #) & f is linear ) by A1, Lm7;
take  G ; ::_thesis: ex H being Ring ex f being Function of G,H st
( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
take  H ; ::_thesis: ex f being Function of G,H st
( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
take  f ; ::_thesis: ( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
thus  ( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear ) by A3; ::_thesis: verum
end;

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 #) & 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 #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
b1 = RingMorphismStr(# G1,G3,(g * f) #)
proof
consider G19, G29, G39 being Ring such that
A2: G19 <= G29 and
A3: ( G29 <= G39 & RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) is Morphism of G29,G39 ) and
A4: RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is Morphism of G19,G29 by A1, Th2;
consider g9 being Function of G29,G39 such that
A5: RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G29,G39,g9 #) and
A6: g9 is linear by A3, Lm7;
consider f9 being Function of G19,G29 such that
A7: RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G19,G29,f9 #) and
A8: f9 is linear by A2, A4, Lm7;
 g9 * f9 is linear by A6, A8, Th1;
then reconsider T9 = RingMorphismStr(# G19,G39,(g9 * f9) #) as strict RingMorphism by Lm5;
take  T9 ; ::_thesis: 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 #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
T9 = RingMorphismStr(# G1,G3,(g * f) #)
thus  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 #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
T9 = RingMorphismStr(# G1,G3,(g * f) #) by A5, A7; ::_thesis: verum
end;
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 #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
b1 = RingMorphismStr(# G1,G3,(g * f) #) ) & ( 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 #) & 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
proof
consider G19, G299 being Ring such that
 G19 <= G299 and
A9: dom F = G19 and
A10: cod F = G299 and
A11: RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is Morphism of G19,G299 by Lm6;
reconsider F9 = RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) as Morphism of G19,G299 by A11;
let S1, S2 be strict RingMorphism; ::_thesis: ( ( 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 #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
S1 = RingMorphismStr(# G1,G3,(g * f) #) ) & ( 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 #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
S2 = RingMorphismStr(# G1,G3,(g * f) #) ) implies S1 = S2 )
assume that
A12: 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 #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
S1 = RingMorphismStr(# G1,G3,(g * f) #) and
A13: 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 #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds
S2 = RingMorphismStr(# G1,G3,(g * f) #) ; ::_thesis: S1 = S2
consider G29, G39 being Ring such that
A14: G29 <= G39 and
A15: dom G = G29 and
 cod G = G39 and
A16: RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) is Morphism of G29,G39 by Lm6;
reconsider F9 = F9 as Morphism of G19,G29 by A1, A15, A10;
consider f9 being Function of G19,G29 such that
A17: F9 = RingMorphismStr(# G19,G29,f9 #) by A1, A15, A9;
reconsider G9 = RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) as Morphism of G29,G39 by A16;
consider g9 being Function of G29,G39 such that
A18: G9 = RingMorphismStr(# G29,G39,g9 #) by A14, Lm8;
thus S1 = RingMorphismStr(# G19,G39,(g9 * f9) #) by A12, A18, A17
.= S2 by A13, A18, A17 ; ::_thesis: verum
end;
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 #) & 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 & G2 <= G3 holds
G1 <= G3
proof
let G1, G2, G3 be Ring; ::_thesis: ( G1 <= G2 & G2 <= G3 implies G1 <= G3 )
assume that
A1: G1 <= G2 and
A2: G2 <= G3 ; ::_thesis: G1 <= G3
consider F0 being RingMorphism such that
A3: dom F0 = G1 and
A4: cod F0 = G2 by A1, Def7;
reconsider F = RingMorphismStr(# the Dom of F0, the Cod of F0, the Fun of F0 #) as RingMorphism by Lm2;
 ( dom F = G1 & cod F = G2 ) by A3, A4;
then reconsider F9 = F as Morphism of G1,G2 by A1, Def8;
consider f being Function of G1,G2 such that
A5: F9 = RingMorphismStr(# G1,G2,f #) by A1, Lm8;
consider G0 being RingMorphism such that
A6: dom G0 = G2 and
A7: cod G0 = G3 by A2, Def7;
reconsider G = RingMorphismStr(# the Dom of G0, the Cod of G0, the Fun of G0 #) as RingMorphism by Lm2;
 ( dom G = G2 & cod G = G3 ) by A6, A7;
then reconsider G9 = G as Morphism of G2,G3 by A2, Def8;
consider g being Function of G2,G3 such that
A8: G9 = RingMorphismStr(# G2,G3,g #) by A2, Lm8;
 dom G = cod F by A4, A6;
then  G * F = RingMorphismStr(# G1,G3,(g * f) #) by A8, A5, Def9;
then  ( dom (G * F) = G1 & cod (G * F) = G3 ) ;
hence  G1 <= G3 by Def7; ::_thesis: verum
end;

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 & G2 <= G3 holds
G * F is Morphism of G1,G3
proof
let G2, G3, G1 be Ring; ::_thesis: for G being Morphism of G2,G3
for F being Morphism of G1,G2 st G1 <= G2 & G2 <= G3 holds
G * F is Morphism of G1,G3
let G be Morphism of G2,G3; ::_thesis: for F being Morphism of G1,G2 st G1 <= G2 & G2 <= G3 holds
G * F is Morphism of G1,G3
let F be Morphism of G1,G2; ::_thesis: ( G1 <= G2 & G2 <= G3 implies G * F is Morphism of G1,G3 )
assume that
A1: G1 <= G2 and
A2: G2 <= G3 ; ::_thesis: G * F is Morphism of G1,G3
consider g being Function of G2,G3 such that
A3: G = RingMorphismStr(# G2,G3,g #) by A2, Lm8;
consider f being Function of G1,G2 such that
A4: F = RingMorphismStr(# G1,G2,f #) by A1, Lm8;
dom G = G2 by A2, Def8
.= cod F by A1, Def8 ;
then  G * F = RingMorphismStr(# G1,G3,(g * f) #) by A3, A4, Def9;
then A5: ( dom (G * F) = G1 & cod (G * F) = G3 ) ;
 G1 <= G3 by A1, A2, Th5;
hence  G * F is Morphism of G1,G3 by A5, Def8; ::_thesis: verum
end;

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 & 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 & 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 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) )
proof
let f, g be strict RingMorphism; ::_thesis: ( dom g = cod f implies 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 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) ) )
assume A1: dom g = cod f ; ::_thesis: 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 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) )
set G1 = dom f;
set G2 = cod f;
set G3 = cod g;
reconsider g9 = g as Morphism of cod f, cod g by A1, Th3;
consider g0 being Function of (cod f),(cod g) such that
A2: g9 = RingMorphismStr(# (cod f),(cod g),g0 #) by A1;
reconsider f9 = f as Morphism of dom f, cod f by Th3;
consider f0 being Function of (dom f),(cod f) such that
A3: f9 = RingMorphismStr(# (dom f),(cod f),f0 #) ;
take  dom f ; ::_thesis: ex G2, G3 being Ring ex f0 being Function of (dom f),G2 ex g0 being Function of G2,G3 st
( f = RingMorphismStr(# (dom f),G2,f0 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# (dom f),G3,(g0 * f0) #) )
take  cod f ; ::_thesis: ex G3 being Ring ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),G3 st
( f = RingMorphismStr(# (dom f),(cod f),f0 #) & g = RingMorphismStr(# (cod f),G3,g0 #) & g * f = RingMorphismStr(# (dom f),G3,(g0 * f0) #) )
take  cod g ; ::_thesis: ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),(cod g) st
( f = RingMorphismStr(# (dom f),(cod f),f0 #) & g = RingMorphismStr(# (cod f),(cod g),g0 #) & g * f = RingMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take  f0 ; ::_thesis: ex g0 being Function of (cod f),(cod g) st
( f = RingMorphismStr(# (dom f),(cod f),f0 #) & g = RingMorphismStr(# (cod f),(cod g),g0 #) & g * f = RingMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take  g0 ; ::_thesis: ( f = RingMorphismStr(# (dom f),(cod f),f0 #) & g = RingMorphismStr(# (cod f),(cod g),g0 #) & g * f = RingMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
thus  ( f = RingMorphismStr(# (dom f),(cod f),f0 #) & g = RingMorphismStr(# (cod f),(cod g),g0 #) & g * f = RingMorphismStr(# (dom f),(cod g),(g0 * f0) #) ) by A1, A3, A2, Def9; ::_thesis: verum
end;

theorem Th8: :: RINGCAT1:8
for f, g being strict RingMorphism st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )
proof
let f, g be strict RingMorphism; ::_thesis: ( dom g = cod f implies ( dom (g * f) = dom f & cod (g * f) = cod g ) )
assume  dom g = cod f ; ::_thesis: ( dom (g * f) = dom f & cod (g * f) = cod g )
then A1: 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 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) ) by Th7;
hence  dom (g * f) = dom f ; ::_thesis: cod (g * f) = cod g
thus  cod (g * f) = cod g by A1; ::_thesis: verum
end;

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 & G2 <= G3 & G3 <= G4 holds
h * (g * f) = (h * g) * f
proof
let G1, G2, G3, G4 be Ring; ::_thesis: for f being Morphism of G1,G2
for g being Morphism of G2,G3
for h being Morphism of G3,G4 st G1 <= G2 & G2 <= G3 & G3 <= G4 holds
h * (g * f) = (h * g) * f
let f be Morphism of G1,G2; ::_thesis: for g being Morphism of G2,G3
for h being Morphism of G3,G4 st G1 <= G2 & G2 <= G3 & G3 <= G4 holds
h * (g * f) = (h * g) * f
let g be Morphism of G2,G3; ::_thesis: for h being Morphism of G3,G4 st G1 <= G2 & G2 <= G3 & G3 <= G4 holds
h * (g * f) = (h * g) * f
let h be Morphism of G3,G4; ::_thesis: ( G1 <= G2 & G2 <= G3 & G3 <= G4 implies h * (g * f) = (h * g) * f )
assume that
A1: G1 <= G2 and
A2: G2 <= G3 and
A3: G3 <= G4 ; ::_thesis: h * (g * f) = (h * g) * f
consider f0 being Function of G1,G2 such that
A4: f = RingMorphismStr(# G1,G2,f0 #) by A1, Lm8;
consider h0 being Function of G3,G4 such that
A5: h = RingMorphismStr(# G3,G4,h0 #) by A3, Lm8;
consider g0 being Function of G2,G3 such that
A6: g = RingMorphismStr(# G2,G3,g0 #) by A2, Lm8;
A7: cod g = G3 by A6;
A8: dom h = G3 by A5;
then A9: h * g = RingMorphismStr(# G2,G4,(h0 * g0) #) by A6, A5, A7, Def9;
A10: dom g = G2 by A6;
then A11: dom (h * g) = G2 by A7, A8, Th8;
A12: cod f = G2 by A4;
then A13: cod (g * f) = G3 by A10, A7, Th8;
 g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) by A4, A6, A12, A10, Def9;
then h * (g * f) = RingMorphismStr(# G1,G4,(h0 * (g0 * f0)) #) by A5, A8, A13, Def9
.= RingMorphismStr(# G1,G4,((h0 * g0) * f0) #) by RELAT_1:36
.= (h * g) * f by A4, A12, A9, A11, Def9 ;
hence  h * (g * f) = (h * g) * f ; ::_thesis: verum
end;

theorem Th10: :: RINGCAT1:10
for f, g, h being strict RingMorphism st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
proof
let f, g, h be strict RingMorphism; ::_thesis: ( dom h = cod g & dom g = cod f implies h * (g * f) = (h * g) * f )
assume that
A1: dom h = cod g and
A2: dom g = cod f ; ::_thesis: h * (g * f) = (h * g) * f
set G1 = dom f;
set G2 = cod f;
set G3 = cod g;
set G4 = cod h;
reconsider h9 = h as Morphism of cod g, cod h by A1, Th3;
reconsider f9 = f as Morphism of dom f, cod f by Th3;
reconsider g9 = g as Morphism of cod f, cod g by A2, Th3;
A3: dom f <= cod f by Th3;
 ( cod f <= cod g & cod g <= cod h ) by A1, A2, Th3;
then  h9 * (g9 * f9) = (h9 * g9) * f9 by A3, Th9;
hence  h * (g * f) = (h * g) * f ; ::_thesis: verum
end;

theorem :: RINGCAT1:11
for G being Ring holds
( dom (ID G) = G & cod (ID G) = G & ( for f being strict RingMorphism st cod f = G holds
(ID G) * f = f ) & ( for g being strict RingMorphism st dom g = G holds
g * (ID G) = g ) )
proof
let G be Ring; ::_thesis: ( dom (ID G) = G & cod (ID G) = G & ( for f being strict RingMorphism st cod f = G holds
(ID G) * f = f ) & ( for g being strict RingMorphism st dom g = G holds
g * (ID G) = g ) )
set i = ID G;
thus A1: ( dom (ID G) = G & cod (ID G) = G ) ; ::_thesis: ( ( for f being strict RingMorphism st cod f = G holds
(ID G) * f = f ) & ( for g being strict RingMorphism st dom g = G holds
g * (ID G) = g ) )
thus  for f being strict RingMorphism st cod f = G holds
(ID G) * f = f ::_thesis: for g being strict RingMorphism st dom g = G holds
g * (ID G) = g
proof
let f be strict RingMorphism; ::_thesis: ( cod f = G implies (ID G) * f = f )
assume A2: cod f = G ; ::_thesis: (ID G) * f = f
set H = dom f;
reconsider f9 = f as Morphism of dom f,G by A2, Th3;
consider m being Function of (dom f),G such that
A3: f9 = RingMorphismStr(# (dom f),G,m #) by A2;
 (id G) * m = m by FUNCT_2:17;
hence  (ID G) * f = f by A1, A2, A3, Def9; ::_thesis: verum
end;
thus  for g being strict RingMorphism st dom g = G holds
g * (ID G) = g ::_thesis: verum
proof
let f be strict RingMorphism; ::_thesis: ( dom f = G implies f * (ID G) = f )
assume A4: dom f = G ; ::_thesis: f * (ID G) = f
set H = cod f;
reconsider f9 = f as Morphism of G, cod f by A4, Th3;
consider m being Function of G,(cod f) such that
A5: f9 = RingMorphismStr(# G,(cod f),m #) by A4;
 m * (id G) = m by FUNCT_2:17;
hence  f * (ID G) = f by A1, A4, A5, Def9; ::_thesis: verum
end;
end;

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 & not b1 is empty )
proof
set X = the strict Ring;
set D = { the strict Ring};
take  { the strict Ring} ; ::_thesis: ( { the strict Ring} is Ring_DOMAIN-like & not { the strict Ring} is empty )
 for x being Element of { the strict Ring} holds x is strict Ring by TARSKI:def_1;
hence  ( { the strict Ring} is Ring_DOMAIN-like & not { the strict Ring} is empty ) by Def11; ::_thesis: verum
end;
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
proof
set e = the Element of V;
 the Element of V is strict Ring by Def11;
hence  ex b1 being Element of V st b1 is strict ; ::_thesis: verum
end;
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
proof
set G = the Ring;
take  {(ID the Ring)} ; ::_thesis: {(ID the Ring)} is RingMorphism_DOMAIN-like
 for x being set st x in {(ID the Ring)} holds
x is strict RingMorphism by TARSKI:def_1;
hence  {(ID the Ring)} is RingMorphism_DOMAIN-like by Def12; ::_thesis: verum
end;
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
proof
set m = the Element of M;
 the Element of M is strict RingMorphism by Def12;
hence  ex b1 being Element of M st b1 is strict ; ::_thesis: verum
end;
end;

theorem Th12: :: RINGCAT1:12
for f being strict RingMorphism holds {f} is RingMorphism_DOMAIN
proof
let f be strict RingMorphism; ::_thesis: {f} is RingMorphism_DOMAIN
 for x being set st x in {f} holds
x is strict RingMorphism by TARSKI:def_1;
hence  {f} is RingMorphism_DOMAIN by Def12; ::_thesis: verum
end;

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
proof
set F = the Morphism of G,H;
reconsider D = { the Morphism of G,H} as RingMorphism_DOMAIN by Th12;
take  D ; ::_thesis: for x being Element of D holds x is Morphism of G,H
thus  for x being Element of D holds x is Morphism of G,H by TARSKI:def_1; ::_thesis: verum
end;
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 )
proof
let D be non empty set ; ::_thesis: 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 )
let G, H be Ring; ::_thesis: ( D is RingMorphism_DOMAIN of G,H iff for x being Element of D holds x is Morphism of G,H )
thus  ( D is RingMorphism_DOMAIN of G,H implies for x being Element of D holds x is Morphism of G,H ) by Def13; ::_thesis: ( ( for x being Element of D holds x is Morphism of G,H ) implies D is RingMorphism_DOMAIN of G,H )
thus  ( ( for x being Element of D holds x is Morphism of G,H ) implies D is RingMorphism_DOMAIN of G,H ) ::_thesis: verum
proof
assume A1: for x being Element of D holds x is Morphism of G,H ; ::_thesis: D is RingMorphism_DOMAIN of G,H
then  for x being set st x in D holds
x is strict RingMorphism ;
then reconsider D9 = D as RingMorphism_DOMAIN by Def12;
 for x being Element of D9 holds x is Morphism of G,H by A1;
hence  D is RingMorphism_DOMAIN of G,H by Def13; ::_thesis: verum
end;
end;

theorem :: RINGCAT1:14
for G, H being Ring
for f being Morphism of G,H holds {f} is RingMorphism_DOMAIN of G,H
proof
let G, H be Ring; ::_thesis: for f being Morphism of G,H holds {f} is RingMorphism_DOMAIN of G,H
let f be Morphism of G,H; ::_thesis: {f} is RingMorphism_DOMAIN of G,H
 for x being Element of {f} holds x is Morphism of G,H by TARSKI:def_1;
hence  {f} is RingMorphism_DOMAIN of G,H by Th13; ::_thesis: verum
end;

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 )
proof
set F = the Morphism of G,H;
set D =  {  RingMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is linear  }  ;
consider f being Function of G,H such that
 the Morphism of G,H = RingMorphismStr(# G,H,f #) and
A2: f is linear by A1, Lm7;
reconsider f0 = f as Element of Maps (G,H) by FUNCT_2:8;
 RingMorphismStr(# G,H,f0 #) in  {  RingMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is linear  }  by A2;
then reconsider D =  {  RingMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is linear  }  as non empty set ;
A3: for x being set st x in D holds
x is Morphism of G,H
proof
let x be set ; ::_thesis: ( x in D implies x is Morphism of G,H )
assume  x in D ; ::_thesis: x is Morphism of G,H
then  ex f being Element of Maps (G,H) st
( x = RingMorphismStr(# G,H,f #) & f is linear ) ;
hence  x is Morphism of G,H by Lm5; ::_thesis: verum
end;
then A4: for x being Element of D holds x is Morphism of G,H ;
A5: for x being set st x is Morphism of G,H holds
x in D
proof
let x be set ; ::_thesis: ( x is Morphism of G,H implies x in D )
assume  x is Morphism of G,H ; ::_thesis: x in D
then reconsider x = x as Morphism of G,H ;
A6: ( dom x = G & cod x = H ) by A1, Def8;
then reconsider f = the Fun of x as Function of G,H ;
reconsider g = f as Element of Maps (G,H) by FUNCT_2:8;
A7: x = RingMorphismStr(# G,H,g #) by A6;
 the Fun of x is linear by Lm3;
hence  x in D by A7; ::_thesis: verum
end;
reconsider D = D as RingMorphism_DOMAIN of G,H by A4, Th13;
take  D ; ::_thesis: for x being set holds
( x in D iff x is Morphism of G,H )
thus  for x being set holds
( x in D iff x is Morphism of G,H ) by A3, A5; ::_thesis: verum
end;
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 ) ) & ( for x being set holds
( x in b2 iff x is Morphism of G,H ) ) holds
b1 = b2
proof
let D1, D2 be RingMorphism_DOMAIN of G,H; ::_thesis: ( ( for x being set holds
( x in D1 iff x is Morphism of G,H ) ) & ( for x being set holds
( x in D2 iff x is Morphism of G,H ) ) implies D1 = D2 )
assume that
A8: for x being set holds
( x in D1 iff x is Morphism of G,H ) and
A9: for x being set holds
( x in D2 iff x is Morphism of G,H ) ; ::_thesis: D1 = D2
 for x being set holds
( x in D1 iff x in D2 )
proof
let x be set ; ::_thesis: ( x in D1 iff x in D2 )
hereby  ::_thesis: ( x in D2 implies x in D1 )
assume  x in D1 ; ::_thesis: x in D2
then  x is Morphism of G,H by A8;
hence  x in D2 by A9; ::_thesis: verum
end;
assume  x in D2 ; ::_thesis: x in D1
then  x is Morphism of G,H by A9;
hence  x in D1 by A8; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
end;
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
proof
set e = the Element of M;
 the Element of M is Morphism of G,H ;
hence  ex b1 being Element of M st b1 is strict ; ::_thesis: verum
end;
end;

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] & ex G being strict Ring st
( y = 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 ) );
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] & ex G being strict Ring st
( y = 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 ) ) );

theorem Th15: :: RINGCAT1:15
for x, y1, y2 being set st GO x,y1 & GO x,y2 holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( GO x,y1 & GO x,y2 implies y1 = y2 )
assume that
A1: GO x,y1 and
A2: GO x,y2 ; ::_thesis: y1 = y2
consider a1, a2, a3, a4, a5, a6 being set  such that
A3: x = [[a1,a2,a3,a4],a5,a6] and
A4: ex G being strict Ring st
( y1 = G & a1 = the carrier of G & a2 = the addF of G & a3 = comp G & a4 = 0. G & a5 = the multF of G & a6 = 1. G ) by A1, Def15;
consider b1, b2, b3, b4, b5, b6 being set  such that
A5: x = [[b1,b2,b3,b4],b5,b6] and
A6: ex G being strict Ring st
( y2 = G & b1 = the carrier of G & b2 = the addF of G & b3 = comp G & b4 = 0. G & b5 = the multF of G & b6 = 1. G ) by A2, Def15;
consider G2 being strict Ring such that
A7: y2 = G2 and
A8: ( b1 = the carrier of G2 & b2 = the addF of G2 ) and
 b3 = comp G2 and
A9: b4 = 0. G2 and
A10: ( b5 = the multF of G2 & b6 = 1. G2 ) by A6;
consider G1 being strict Ring such that
A11: y1 = G1 and
A12: ( a1 = the carrier of G1 & a2 = the addF of G1 ) and
 a3 = comp G1 and
A13: a4 = 0. G1 and
A14: ( a5 = the multF of G1 & a6 = 1. G1 ) by A4;
A15: ( the multF of G1 = the multF of G2 & 1. G1 = 1. G2 ) by A3, A5, A14, A10, XTUPLE_0:3;
A16: [a1,a2,a3,a4] = [b1,b2,b3,b4] by A3, A5, XTUPLE_0:3;
then  ( the carrier of G1 = the carrier of G2 & the addF of G1 = the addF of G2 ) by A12, A8, XTUPLE_0:5;
hence  y1 = y2 by A11, A13, A7, A9, A16, A15, XTUPLE_0:5; ::_thesis: verum
end;

theorem Th16: :: RINGCAT1:16
for UN being Universe ex x being set st
( x in UN & GO x, Z_3 )
proof
let UN be Universe; ::_thesis: ex x being set st
( x in UN & GO x, Z_3 )
set G = Z_3 ;
reconsider x1 = the carrier of Z_3, x2 = the addF of Z_3, x3 = comp Z_3, x4 = 0. Z_3, x5 = the multF of Z_3, x6 = 1. Z_3 as Element of UN by MOD_2:29;
set x9 = [x1,x2,x3,x4];
set x = [[x1,x2,x3,x4],x5,x6];
A1: GO [[x1,x2,x3,x4],x5,x6], Z_3
proof
take  x1 ; :: according to RINGCAT1:def_15 ::_thesis: ex x2, x3, x4, x5, x6 being set st
( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z_3 = 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 ) )
take  x2 ; ::_thesis: ex x3, x4, x5, x6 being set st
( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z_3 = 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 ) )
take  x3 ; ::_thesis: ex x4, x5, x6 being set st
( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z_3 = 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 ) )
take  x4 ; ::_thesis: ex x5, x6 being set st
( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z_3 = 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 ) )
take  x5 ; ::_thesis: ex x6 being set st
( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z_3 = 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 ) )
take  x6 ; ::_thesis: ( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z_3 = 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 ) )
thus  ( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z_3 = 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 ) ) ; ::_thesis: verum
end;
take  [[x1,x2,x3,x4],x5,x6] ; ::_thesis: ( [[x1,x2,x3,x4],x5,x6] in UN & GO [[x1,x2,x3,x4],x5,x6], Z_3 )
 [x1,x2,x3,x4] is Element of UN by GRCAT_1:1;
hence  ( [[x1,x2,x3,x4],x5,x6] in UN & GO [[x1,x2,x3,x4],x5,x6], Z_3 ) by A1, GRCAT_1:1; ::_thesis: verum
end;

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 & 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 & GO x,y ) )
proof
defpred S1[ set , set ] means  GO $1,$2;
A1: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2 by Th15;
consider Y being set  such that
A2: for y being set holds
( y in Y iff ex x being set st
( x in UN & S1[x,y] ) ) from TARSKI:sch_1(A1);
take  Y ; ::_thesis: for y being set holds
( y in Y iff ex x being set st
( x in UN & GO x,y ) )
thus  for y being set holds
( y in Y iff ex x being set st
( x in UN & GO x,y ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st
( x in UN & GO x,y ) ) ) & ( for y being set holds
( y in b2 iff ex x being set st
( x in UN & GO x,y ) ) ) holds
b1 = b2
proof
let Y1, Y2 be set ; ::_thesis: ( ( for y being set holds
( y in Y1 iff ex x being set st
( x in UN & GO x,y ) ) ) & ( for y being set holds
( y in Y2 iff ex x being set st
( x in UN & GO x,y ) ) ) implies Y1 = Y2 )
assume that
A3: for y being set holds
( y in Y1 iff ex x being set st
( x in UN & GO x,y ) ) and
A4: for y being set holds
( y in Y2 iff ex x being set st
( x in UN & GO x,y ) ) ; ::_thesis: Y1 = Y2
now__::_thesis:_for_y_being_set_holds_
(_y_in_Y1_iff_y_in_Y2_)
let y be set ; ::_thesis: ( y in Y1 iff y in Y2 )
 ( y in Y1 iff ex x being set st
( x in UN & GO x,y ) ) by A3;
hence  ( y in Y1 iff y in Y2 ) by A4; ::_thesis: verum
end;
hence  Y1 = Y2 by TARSKI:1; ::_thesis: verum
end;
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 & GO x,y ) ) );

theorem Th17: :: RINGCAT1:17
for UN being Universe holds Z_3 in RingObjects UN
proof
let UN be Universe; ::_thesis: Z_3 in RingObjects UN
 ex x being set st
( x in UN & GO x, Z_3 ) by Th16;
hence  Z_3 in RingObjects UN by Def16; ::_thesis: verum
end;

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
proof
let UN be Universe; ::_thesis: for x being Element of RingObjects UN holds x is strict Ring
let x be Element of RingObjects UN; ::_thesis: x is strict Ring
consider u being set  such that
 u in UN and
A1: GO u,x by Def16;
 ex x1, x2, x3, x4, x5, x6 being set st
( u = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( x = 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, Def15;
hence  x is strict Ring ; ::_thesis: verum
end;

registration
let UN be Universe;
cluster RingObjects UN ->  Ring_DOMAIN-like ;
coherence
 RingObjects UN is Ring_DOMAIN-like
proof
 for x being Element of RingObjects UN holds x is strict Ring by Th18;
hence  RingObjects UN is Ring_DOMAIN-like by Def11; ::_thesis: verum
end;
end;

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 & 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 & x is Morphism of G,H ) )
proof
set G0 = the Element of V;
set M = Morphs ( the Element of V, the Element of V);
set S =  {  (Morphs (G,H)) where G, H is Element of V : G <= H  }  ;
 ( ID the Element of V is Element of Morphs ( the Element of V, the Element of V) & Morphs ( the Element of V, the Element of V) in  {  (Morphs (G,H)) where G, H is Element of V : G <= H  }  ) by Def14;
then reconsider T = union  {  (Morphs (G,H)) where G, H is Element of V : G <= H  }  as non empty set by TARSKI:def_4;
A1: for x being set holds
( x in T iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
proof
let x be set ; ::_thesis: ( x in T iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
thus  ( x in T implies ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) ::_thesis: ( ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) implies x in T )
proof
assume  x in T ; ::_thesis: ex G, H being Element of V st
( G <= H & x is Morphism of G,H )
then consider Y being set  such that
A2: x in Y and
A3: Y in  {  (Morphs (G,H)) where G, H is Element of V : G <= H  }  by TARSKI:def_4;
consider G, H being Element of V such that
A4: Y = Morphs (G,H) and
A5: G <= H by A3;
take  G ; ::_thesis: ex H being Element of V st
( G <= H & x is Morphism of G,H )
take  H ; ::_thesis: ( G <= H & x is Morphism of G,H )
 x is Element of Morphs (G,H) by A2, A4;
hence  ( G <= H & x is Morphism of G,H ) by A5; ::_thesis: verum
end;
thus  ( ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) implies x in T ) ::_thesis: verum
proof
given G, H being Element of V such that A6: ( G <= H & x is Morphism of G,H ) ; ::_thesis: x in T
set M = Morphs (G,H);
 ( x in Morphs (G,H) & Morphs (G,H) in  {  (Morphs (G,H)) where G, H is Element of V : G <= H  }  ) by A6, Def14;
hence  x in T by TARSKI:def_4; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_set_st_x_in_T_holds_
x_is_strict_RingMorphism
let x be set ; ::_thesis: ( x in T implies x is strict RingMorphism )
assume  x in T ; ::_thesis: x is strict RingMorphism
then  ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) by A1;
hence  x is strict RingMorphism ; ::_thesis: verum
end;
then reconsider T9 = T as RingMorphism_DOMAIN by Def12;
take  T9 ; ::_thesis: for x being set holds
( x in T9 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
thus  for x being set holds
( x in T9 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) by A1; ::_thesis: verum
end;
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 & x is Morphism of G,H ) ) ) & ( for x being set holds
( x in b2 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) ) holds
b1 = b2
proof
let D1, D2 be RingMorphism_DOMAIN; ::_thesis: ( ( for x being set holds
( x in D1 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) ) & ( for x being set holds
( x in D2 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) ) implies D1 = D2 )
assume that
A7: for x being set holds
( x in D1 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) and
A8: for x being set holds
( x in D2 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) ; ::_thesis: D1 = D2
now__::_thesis:_for_x_being_set_holds_
(_x_in_D1_iff_x_in_D2_)
let x be set ; ::_thesis: ( x in D1 iff x in D2 )
 ( x in D1 iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) by A7;
hence  ( x in D1 iff x in D2 ) by A8; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
end;
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 & x is Morphism of G,H ) ) );

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
proof
consider G, H being Element of V such that
A1: G <= H and
A2: F is Morphism of G,H by Def17;
reconsider F9 = F as Morphism of G,H by A2;
 dom F9 = G by A1, Def8;
hence  dom F is Element of V ; ::_thesis: verum
end;
:: original: cod
redefine func cod F ->  Element of V;
coherence
 cod F is Element of V
proof
consider G, H being Element of V such that
A3: G <= H and
A4: F is Morphism of G,H by Def17;
reconsider F9 = F as Morphism of G,H by A4;
 cod F9 = H by A3, Def8;
hence  cod F is Element of V ; ::_thesis: verum
end;
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
proof
deffunc H1( Element of Morphs V) ->  Element of V = dom $1;
consider F being Function of (Morphs V),V such that
A1: for f being Element of Morphs V holds F . f = H1(f) from FUNCT_2:sch_4();
take  F ; ::_thesis: for f being Element of Morphs V holds F . f = dom f
thus  for f being Element of Morphs V holds F . f = dom f by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = dom f ) & ( for f being Element of Morphs V holds b2 . f = dom f ) holds
b1 = b2
proof
let F1, F2 be Function of (Morphs V),V; ::_thesis: ( ( for f being Element of Morphs V holds F1 . f = dom f ) & ( for f being Element of Morphs V holds F2 . f = dom f ) implies F1 = F2 )
assume that
A2: for f being Element of Morphs V holds F1 . f = dom f and
A3: for f being Element of Morphs V holds F2 . f = dom f ; ::_thesis: F1 = F2
now__::_thesis:_for_f_being_Element_of_Morphs_V_holds_F1_._f_=_F2_._f
let f be Element of Morphs V; ::_thesis: F1 . f = F2 . f
 F1 . f = dom f by A2;
hence  F1 . f = F2 . f by A3; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
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
proof
deffunc H1( Element of Morphs V) ->  Element of V = cod $1;
consider F being Function of (Morphs V),V such that
A4: for f being Element of Morphs V holds F . f = H1(f) from FUNCT_2:sch_4();
take  F ; ::_thesis: for f being Element of Morphs V holds F . f = cod f
thus  for f being Element of Morphs V holds F . f = cod f by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = cod f ) & ( for f being Element of Morphs V holds b2 . f = cod f ) holds
b1 = b2
proof
let F1, F2 be Function of (Morphs V),V; ::_thesis: ( ( for f being Element of Morphs V holds F1 . f = cod f ) & ( for f being Element of Morphs V holds F2 . f = cod f ) implies F1 = F2 )
assume that
A5: for f being Element of Morphs V holds F1 . f = cod f and
A6: for f being Element of Morphs V holds F2 . f = cod f ; ::_thesis: F1 = F2
now__::_thesis:_for_f_being_Element_of_Morphs_V_holds_F1_._f_=_F2_._f
let f be Element of Morphs V; ::_thesis: F1 . f = F2 . f
 F1 . f = cod f by A5;
hence  F1 . f = F2 . f by A6; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
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;

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 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 )
proof
let V be Ring_DOMAIN; ::_thesis: 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 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 )
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom $1 = cod $2;
let g, f be Element of Morphs V; ::_thesis: ( dom g = cod f implies ex G1, G2, G3 being Element of V st
( G1 <= G2 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 ) )
assume A1: S1[g,f] ; ::_thesis: ex G1, G2, G3 being Element of V st
( G1 <= G2 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 )
consider G2, G3 being Element of V such that
A2: ( G2 <= G3 & g is Morphism of G2,G3 ) by Def17;
consider G1, G29 being Element of V such that
A3: ( G1 <= G29 & f is Morphism of G1,G29 ) by Def17;
A4: G29 = cod f by A3, Def8;
 G2 = dom g by A2, Def8;
hence  ex G1, G2, G3 being Element of V st
( G1 <= G2 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 ) by A1, A2, A3, A4; ::_thesis: verum
end;

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
proof
let V be Ring_DOMAIN; ::_thesis: for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom $1 = cod $2;
let g, f be Element of Morphs V; ::_thesis: ( dom g = cod f implies g * f in Morphs V )
assume  S1[g,f] ; ::_thesis: g * f in Morphs V
then consider G1, G2, G3 being Element of V such that
A1: ( G1 <= G2 & G2 <= G3 ) and
A2: g is Morphism of G2,G3 and
A3: f is Morphism of G1,G2 by Th19;
reconsider f9 = f as Morphism of G1,G2 by A3;
reconsider g9 = g as Morphism of G2,G3 by A2;
 ( G1 <= G3 & g9 *' f9 = g9 * f9 ) by A1, Def10, Th5;
hence  g * f in Morphs V by Def17; ::_thesis: verum
end;

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 ) ) & ( 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 ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) )
proof
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom $1 = cod $2;
deffunc H1( Element of Morphs V, Element of Morphs V) ->  strict RingMorphism = $1 * $2;
A1: for g, f being Element of Morphs V st S1[g,f] holds
H1(g,f) in Morphs V by Th20;
consider c being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) such that
A2: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff S1[g,f] ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = H1(g,f) ) ) from BINOP_1:sch_8(A1);
take  c ; ::_thesis: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = g * f ) )
thus  ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = g * f ) ) by A2; ::_thesis: verum
end;
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 ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . (g,f) = g * f ) holds
b1 = b2
proof
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom $1 = cod $2;
let c1, c2 be PartFunc of [:(Morphs V),(Morphs V):],(Morphs V); ::_thesis: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c1 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c1 holds
c1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom c2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c2 holds
c2 . (g,f) = g * f ) implies c1 = c2 )
assume that
A3: for g, f being Element of Morphs V holds
( [g,f] in dom c1 iff S1[g,f] ) and
A4: for g, f being Element of Morphs V st [g,f] in dom c1 holds
c1 . (g,f) = g * f and
A5: for g, f being Element of Morphs V holds
( [g,f] in dom c2 iff S1[g,f] ) and
A6: for g, f being Element of Morphs V st [g,f] in dom c2 holds
c2 . (g,f) = g * f ; ::_thesis: c1 = c2
set V0 = dom c1;
B9: now__::_thesis:_for_x_being_set_st_x_in_dom_c1_holds_
x_in_dom_c2
let x be set ; ::_thesis: ( x in dom c1 implies x in dom c2 )
assume A7: x in dom c1 ; ::_thesis: x in dom c2
then consider g, f being Element of Morphs V such that
A8: x = [g,f] by SUBSET_1:43;
 S1[g,f] by A3, A7, A8;
hence  x in dom c2 by A5, A8; ::_thesis: verum
end;
then A9: dom c1 c= dom c2 by TARSKI:def_3;
A10: for x, y being set st [x,y] in dom c1 holds
c1 . (x,y) = c2 . (x,y)
proof
let x, y be set ; ::_thesis: ( [x,y] in dom c1 implies c1 . (x,y) = c2 . (x,y) )
assume A11: [x,y] in dom c1 ; ::_thesis: c1 . (x,y) = c2 . (x,y)
then reconsider x = x, y = y as Element of Morphs V by ZFMISC_1:87;
 c1 . (x,y) = x * y by A4, A11;
hence  c1 . (x,y) = c2 . (x,y) by A6, B9, A11; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_c2_holds_
x_in_dom_c1
let x be set ; ::_thesis: ( x in dom c2 implies x in dom c1 )
assume A12: x in dom c2 ; ::_thesis: x in dom c1
then consider g, f being Element of Morphs V such that
A13: x = [g,f] by SUBSET_1:43;
 S1[g,f] by A5, A12, A13;
hence  x in dom c1 by A3, A13; ::_thesis: verum
end;
then  dom c2 c= dom c1 by TARSKI:def_3;
hence  c1 = c2 by A10, BINOP_1:20, A9, XBOOLE_0:def_10; ::_thesis: verum
end;
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 ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . (g,f) = g * f ) ) );

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 & not RingCat UN is void & 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 )
proof
let UN be Universe; ::_thesis: for f, g being Morphism of (RingCat UN) holds
( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f )
set C = RingCat UN;
set V = RingObjects UN;
let f, g be Morphism of (RingCat UN); ::_thesis: ( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f )
reconsider f9 = f as Element of Morphs (RingObjects UN) ;
reconsider g9 = g as Element of Morphs (RingObjects UN) ;
 ( dom g = dom g9 & cod f = cod f9 ) by Def19, Def20;
hence  ( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f ) by Def22; ::_thesis: verum
end;

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) & f9 is Morphism of (RingCat UN) & b is strict Element of RingObjects UN & b9 is Object of (RingCat UN) )
proof
let UN be Universe; ::_thesis: 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); ::_thesis: 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); ::_thesis: 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); ::_thesis: 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; ::_thesis: ( 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) ; ::_thesis: ( 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) ; ::_thesis: ( 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, Def15;
hence  b is strict Element of RingObjects UN ; ::_thesis: b9 is Object of (RingCat UN)
thus  b9 is Object of (RingCat UN) ; ::_thesis: verum
end;

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 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (RingObjects UN)) ) & ( [g9,f9] in dom (comp (RingObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
proof
let UN be Universe; ::_thesis: for f, g being Morphism of (RingCat UN)
for f9, g9 being Element of Morphs (RingObjects UN) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (RingObjects UN)) ) & ( [g9,f9] in dom (comp (RingObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
set C = RingCat UN;
set V = RingObjects UN;
set X = Morphs (RingObjects UN);
let f, g be Morphism of (RingCat UN); ::_thesis: for f9, g9 being Element of Morphs (RingObjects UN) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (RingObjects UN)) ) & ( [g9,f9] in dom (comp (RingObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
let f9, g9 be Element of Morphs (RingObjects UN); ::_thesis: ( f = f9 & g = g9 implies ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (RingObjects UN)) ) & ( [g9,f9] in dom (comp (RingObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) )
assume that
A1: f = f9 and
A2: g = g9 ; ::_thesis: ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (RingObjects UN)) ) & ( [g9,f9] in dom (comp (RingObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
A3: cod f = cod f9 by A1, Def20;
hence  ( dom g = cod f iff dom g9 = cod f9 ) by A2, Def19; ::_thesis: ( ( dom g = cod f implies [g9,f9] in dom (comp (RingObjects UN)) ) & ( [g9,f9] in dom (comp (RingObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
 dom g = dom g9 by A2, Def19;
hence A4: ( dom g = cod f iff [g9,f9] in dom (comp (RingObjects UN)) ) by A3, Def22; ::_thesis: ( ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
thus  ( dom g = cod f implies g (*) f = g9 * f9 ) ::_thesis: ( ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
proof
assume A5: dom g = cod f ; ::_thesis: g (*) f = g9 * f9
then  [g,f] in dom the Comp of (RingCat UN) by Th21;
hence g (*) f = (comp (RingObjects UN)) . (g9,f9) by A1, A2, CAT_1:def_1
.= g9 * f9 by A4, A5, Def22 ;
::_thesis: verum
end;
 dom f = dom f9 by A1, Def19;
hence  ( dom f = dom g iff dom f9 = dom g9 ) by A2, Def19; ::_thesis: ( cod f = cod g iff cod f9 = cod g9 )
 cod g = cod g9 by A2, Def20;
hence  ( cod f = cod g iff cod f9 = cod g9 ) by A1, Def20; ::_thesis: verum
end;

Lm9:  for UN being Universe
for f, g being Morphism of (RingCat UN) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
proof
let UN be Universe; ::_thesis: for f, g being Morphism of (RingCat UN) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
set X = Morphs (RingObjects UN);
let f, g be Morphism of (RingCat UN); ::_thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
assume A1: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
reconsider g9 = g as strict Element of Morphs (RingObjects UN) by Th22;
reconsider f9 = f as strict Element of Morphs (RingObjects UN) by Th22;
A2: dom g9 = cod f9 by A1, Th24;
then reconsider gf = g9 * f9 as Element of Morphs (RingObjects UN) by Th20;
A3: gf = g (*) f by A1, Th24;
 ( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by A2, Th8;
hence  ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, Th24; ::_thesis: verum
end;

Lm10:  for UN being Universe
for f, g, h being Morphism of (RingCat UN) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
proof
let UN be Universe; ::_thesis: for f, g, h being Morphism of (RingCat UN) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
set X = Morphs (RingObjects UN);
let f, g, h be Morphism of (RingCat UN); ::_thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
assume A1: ( dom h = cod g & dom g = cod f ) ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f
reconsider f9 = f, g9 = g, h9 = h as strict Element of Morphs (RingObjects UN) by Th22;
A2: ( h9 * g9 = h (*) g & dom (h (*) g) = cod f ) by A1, Lm9, Th24;
A3: ( dom h9 = cod g9 & dom g9 = cod f9 ) by A1, Th24;
then reconsider gf = g9 * f9, hg = h9 * g9 as strict Element of Morphs (RingObjects UN) by Th20;
 ( g9 * f9 = g (*) f & dom h = cod (g (*) f) ) by A1, Lm9, Th24;
then h (*) (g (*) f) = h9 * gf by Th24
.= hg * f9 by A3, Th10
.= (h (*) g) (*) f by A2, Th24 ;
hence  h (*) (g (*) f) = (h (*) g) (*) f ; ::_thesis: verum
end;

registration
let UN be Universe;
cluster RingCat UN ->  Category-like transitive associative reflexive ;
coherence
 ( RingCat UN is Category-like & RingCat UN is transitive & RingCat UN is associative & RingCat UN is reflexive )
proof
set C = RingCat UN;
thus  RingCat UN is Category-like ::_thesis: ( RingCat UN is transitive & RingCat UN is associative & RingCat UN is reflexive )
proof
let f be Morphism of (RingCat UN); :: according to CAT_1:def_6 ::_thesis: for b1 being Element of the carrier' of (RingCat UN) holds
( ( not [b1,f] in proj1 the Comp of (RingCat UN) or dom b1 = cod f ) & ( not dom b1 = cod f or [b1,f] in proj1 the Comp of (RingCat UN) ) )
thus  for b1 being Element of the carrier' of (RingCat UN) holds
( ( not [b1,f] in proj1 the Comp of (RingCat UN) or dom b1 = cod f ) & ( not dom b1 = cod f or [b1,f] in proj1 the Comp of (RingCat UN) ) ) by Th21; ::_thesis: verum
end;
thus  RingCat UN is transitive ::_thesis: ( RingCat UN is associative & RingCat UN is reflexive )
proof
let f be Morphism of (RingCat UN); :: according to CAT_1:def_7 ::_thesis: for b1 being Element of the carrier' of (RingCat UN) holds
( not dom b1 = cod f or ( dom (b1 (*) f) = dom f & cod (b1 (*) f) = cod b1 ) )
thus  for b1 being Element of the carrier' of (RingCat UN) holds
( not dom b1 = cod f or ( dom (b1 (*) f) = dom f & cod (b1 (*) f) = cod b1 ) ) by Lm9; ::_thesis: verum
end;
thus  RingCat UN is associative ::_thesis: RingCat UN is reflexive
proof
let f be Morphism of (RingCat UN); :: according to CAT_1:def_8 ::_thesis: for b1, b2 being Element of the carrier' of (RingCat UN) holds
( not dom b2 = cod b1 or not dom b1 = cod f or b2 (*) (b1 (*) f) = (b2 (*) b1) (*) f )
thus  for b1, b2 being Element of the carrier' of (RingCat UN) holds
( not dom b2 = cod b1 or not dom b1 = cod f or b2 (*) (b1 (*) f) = (b2 (*) b1) (*) f ) by Lm10; ::_thesis: verum
end;
thus  RingCat UN is reflexive ::_thesis: verum
proof
let a be Element of (RingCat UN); :: according to CAT_1:def_9 ::_thesis: not Hom (a,a) = {}
reconsider G = a as Element of RingObjects UN ;
consider x being set  such that
 x in UN and
W2: GO x,G by Def16;
set ii = ID G;
consider x1, x2, x3, x4, x5, x6 being set  such that
 x = [[x1,x2,x3,x4],x5,x6] and
W3: ex H being strict Ring st
( G = H & x1 = the carrier of H & x2 = the addF of H & x3 = comp H & x4 = 0. H & x5 = the multF of H & x6 = 1. H ) by W2, Def15;
reconsider G = G as strict Element of RingObjects UN by W3;
reconsider ii = ID G as Morphism of (RingCat UN) ;
reconsider ia = ii as RingMorphismStr ;
A: dom ii = dom ia by Def19
.= a ;
cod ii = cod ia by Def20
.= a ;
then  ii in Hom (a,a) by A;
hence  Hom (a,a) <> {} ; ::_thesis: verum
end;
end;
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 ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
proof
let UN be Universe; ::_thesis: 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 ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
let a be Element of (RingCat UN); ::_thesis: 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 ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
let aa be Element of RingObjects UN; ::_thesis: ( a = aa implies 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 ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) )
assume  a = aa ; ::_thesis: 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 ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
let i be Morphism of a,a; ::_thesis: ( i = ID aa implies for b being Element of (RingCat UN) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) )
assume Z2: i = ID aa ; ::_thesis: for b being Element of (RingCat UN) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
let b be Element of (RingCat UN); ::_thesis: ( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
thus  ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )
proof
assume Z3: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) i = g
let g be Morphism of a,b; ::_thesis: g (*) i = g
reconsider gg = g, ii = i as Element of Morphs (RingObjects UN) ;
consider G1, H1 being Element of RingObjects UN such that
W0: G1 <= H1 and
W1: gg is Morphism of G1,H1 by Def17;
consider f being Function of G1,H1 such that
W2: gg = RingMorphismStr(# G1,H1,f #) by W0, W1, Lm8;
E: Hom (a,a) <> {} by CAT_1:def_9;
CC1: dom g = a by Z3, CAT_1:5
.= cod i by E, CAT_1:5 ;
then C1: dom gg = cod ii by Th24;
then reconsider f = f as Function of aa,H1 by W2, Z2;
A: [gg,ii] in dom (comp (RingObjects UN)) by Th24, CC1;
hence g (*) i = (comp (RingObjects UN)) . (g,i) by CAT_1:def_1
.= gg * ii by A, Def22
.= RingMorphismStr(# aa,H1,(f * (id aa)) #) by Z2, Def9, W2, C1
.= g by Z2, W2, C1, FUNCT_2:17 ;
::_thesis: verum
end;
thus  ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ::_thesis: verum
proof
assume Z3: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds i (*) f = f
let g be Morphism of b,a; ::_thesis: i (*) g = g
reconsider gg = g, ii = i as Element of Morphs (RingObjects UN) ;
consider G1, H1 being Element of RingObjects UN such that
W0: G1 <= H1 and
W1: gg is Morphism of G1,H1 by Def17;
consider f being Function of G1,H1 such that
W2: gg = RingMorphismStr(# G1,H1,f #) by W0, W1, Lm8;
E: Hom (a,a) <> {} by CAT_1:def_9;
CC1: cod g = a by Z3, CAT_1:5
.= dom i by E, CAT_1:5 ;
then C1: cod gg = dom ii by Th24;
reconsider f = f as Function of G1,aa by W2, Z2, C1;
A: [ii,gg] in dom (comp (RingObjects UN)) by CC1, Th24;
hence i (*) g = (comp (RingObjects UN)) . (i,g) by CAT_1:def_1
.= ii * gg by A, Def22
.= RingMorphismStr(# G1,aa,((id aa) * f) #) by Z2, Def9, W2, C1
.= g by Z2, C1, W2, FUNCT_2:17 ;
::_thesis: verum
end;
end;

registration
let UN be Universe;
cluster RingCat UN ->  with_identities ;
coherence
 RingCat UN is with_identities
proof
set C = RingCat UN;
let a be Element of (RingCat UN); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of (RingCat UN) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider aa = a as Element of RingObjects UN ;
reconsider ii = ID aa as Morphism of (RingCat UN) ;
reconsider ia = ii as RingMorphismStr ;
A: dom ii = dom ia by Def19
.= a ;
cod ii = cod ia by Def20
.= a ;
then reconsider ii = ii as Morphism of a,a by A, CAT_1:4;
take  ii ; ::_thesis: for b1 being Element of the carrier of (RingCat UN) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
thus  for b1 being Element of the carrier of (RingCat UN) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) by LmX; ::_thesis: verum
end;
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
proof
let UN be Universe; ::_thesis: for a being Object of (RingCat UN)
for aa being Element of RingObjects UN st a = aa holds
id a = ID aa
let a be Object of (RingCat UN); ::_thesis: for aa being Element of RingObjects UN st a = aa holds
id a = ID aa
let aa be Element of RingObjects UN; ::_thesis: ( a = aa implies id a = ID aa )
set C = RingCat UN;
assume Z: a = aa ; ::_thesis: id a = ID aa
reconsider ii = ID aa as Morphism of (RingCat UN) ;
reconsider ia = ii as RingMorphismStr ;
A: dom ii = dom ia by Def19
.= a by Z ;
cod ii = cod ia by Def20
.= a by Z ;
then reconsider ii = ii as Morphism of a,a by A, CAT_1:4;
 for b being Object of (RingCat UN) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ) by Z, LmX;
hence  id a = ID aa by CAT_1:def_12; ::_thesis: verum
end;