:: RINGCAT1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let G, H be non empty doubleLoopStr ;
let IT be Function of G,H;
canceled;
attr IT is linear means :Def2: :: RINGCAT1:def 2
( ( for x, y being Scalar of G holds IT . (x + y) = (IT . x) + (IT . y) ) & ( for x, y being Scalar of G holds IT . (x * y) = (IT . x) * (IT . y) ) & IT . (1. G) = 1. H );
end;

:: deftheorem RINGCAT1:def 1 :
canceled;

:: deftheorem Def2 defines linear RINGCAT1:def 2 :
for G, H being non empty doubleLoopStr
for IT being Function of G,H holds
( IT is linear iff ( ( for x, y being Scalar of G holds IT . (x + y) = (IT . x) + (IT . y) ) & ( for x, y being Scalar of G holds IT . (x * y) = (IT . x) * (IT . y) ) & IT . (1. G) = 1. H ) );

theorem :: RINGCAT1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RINGCAT1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: RINGCAT1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
attr c1 is strict;
struct RingMorphismStr -> ;
aggr RingMorphismStr(# 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 3
the Dom of f;
coherence
the Dom of f is Ring
;
func cod f -> Ring equals :: RINGCAT1:def 4
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 5
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 3 :
for f being RingMorphismStr holds dom f = the Dom of f;

:: deftheorem defines cod RINGCAT1:def 4 :
for f being RingMorphismStr holds cod f = the Cod of f;

:: deftheorem defines fun RINGCAT1:def 5 :
for f being RingMorphismStr holds fun f = the Fun of f;

Lm1: for G being non empty doubleLoopStr holds id G is linear
proof 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 ;
attr IT is RingMorphism-like means :Def6: :: RINGCAT1:def 6
fun IT is linear;
end;

:: deftheorem Def6 defines RingMorphism-like RINGCAT1:def 6 :
for IT being RingMorphismStr holds
( IT is RingMorphism-like iff fun IT is linear );

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

definition
mode RingMorphism is RingMorphism-like RingMorphismStr ;
end;

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

:: deftheorem defines ID RINGCAT1:def 7 :
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;
pred G <= H means :Def8: :: RINGCAT1:def 8
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 end;
end;

:: deftheorem Def8 defines <= RINGCAT1:def 8 :
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 end;

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

:: deftheorem Def9 defines Morphism RINGCAT1:def 9 :
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 Morphism of G,H;
existence
ex b1 being Morphism of G,H st b1 is strict
proof 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 end;
end;

Lm3: for F being RingMorphism holds the Fun of F is linear
proof 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 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 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 end;

theorem :: RINGCAT1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: RINGCAT1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th6: :: RINGCAT1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being strict RingMorphism holds
( F is Morphism of dom F, cod F & dom F <= cod F )
proof 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 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 end;

theorem :: RINGCAT1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let G, F be RingMorphism;
assume A1: dom G = cod F ;
func G * F -> strict RingMorphism means :Def10: :: RINGCAT1:def 10
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 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 end;
end;

:: deftheorem Def10 defines * RINGCAT1:def 10 :
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 Th8: :: RINGCAT1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2, G3 being Ring st G1 <= G2 & G2 <= G3 holds
G1 <= G3
proof end;

theorem Th9: :: RINGCAT1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 ) ;
func G *' F -> strict Morphism of G1,G3 equals :Def11: :: RINGCAT1:def 11
G * F;
coherence
G * F is strict Morphism of G1,G3
by A1, Th9;
end;

:: deftheorem Def11 defines *' RINGCAT1:def 11 :
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 Th10: :: RINGCAT1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th11: :: RINGCAT1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being strict RingMorphism st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )
proof end;

theorem Th12: :: RINGCAT1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th13: :: RINGCAT1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g, h being strict RingMorphism st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
proof end;

theorem Th14: :: RINGCAT1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let IT be set ;
attr IT is Ring_DOMAIN-like means :Def12: :: RINGCAT1:def 12
for x being Element of IT holds x is strict Ring;
end;

:: deftheorem Def12 defines Ring_DOMAIN-like RINGCAT1:def 12 :
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 set ;
existence
ex b1 being set st
( b1 is Ring_DOMAIN-like & not b1 is empty )
proof 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 Def12;
end;

registration
let V be Ring_DOMAIN;
cluster strict Element of V;
existence
ex b1 being Element of V st b1 is strict
proof end;
end;

definition
let IT be set ;
attr IT is RingMorphism_DOMAIN-like means :Def13: :: RINGCAT1:def 13
for x being set st x in IT holds
x is strict RingMorphism;
end;

:: deftheorem Def13 defines RingMorphism_DOMAIN-like RINGCAT1:def 13 :
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 set ;
existence
ex b1 being non empty set st b1 is RingMorphism_DOMAIN-like
proof 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 Def13;
end;

registration
let M be RingMorphism_DOMAIN;
cluster strict Element of M;
existence
ex b1 being Element of M st b1 is strict
proof end;
end;

theorem :: RINGCAT1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RINGCAT1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th17: :: RINGCAT1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being strict RingMorphism holds {f} is RingMorphism_DOMAIN
proof end;

definition
let G, H be Ring;
mode RingMorphism_DOMAIN of G,H -> RingMorphism_DOMAIN means :Def14: :: RINGCAT1:def 14
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 end;
end;

:: deftheorem Def14 defines RingMorphism_DOMAIN RINGCAT1:def 14 :
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 Th18: :: RINGCAT1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RINGCAT1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, H being Ring
for f being Morphism of G,H holds {f} is RingMorphism_DOMAIN of G,H
proof end;

definition
let G, H be Ring;
assume A1: G <= H ;
func Morphs G,H -> RingMorphism_DOMAIN of G,H means :Def15: :: RINGCAT1:def 15
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 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 end;
end;

:: deftheorem Def15 defines Morphs RINGCAT1:def 15 :
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 Def14;
end;

registration
let G, H be Ring;
let M be RingMorphism_DOMAIN of G,H;
cluster strict Element of M;
existence
ex b1 being Element of M st b1 is strict
proof end;
end;

definition
let x, y be set ;
pred GO x,y means :Def16: :: RINGCAT1:def 16
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 add of G & x3 = comp G & x4 = the Zero of G & x5 = the mult of G & x6 = the unity of G ) );
end;

:: deftheorem Def16 defines GO RINGCAT1:def 16 :
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 add of G & x3 = comp G & x4 = the Zero of G & x5 = the mult of G & x6 = the unity of G ) ) );

theorem Th20: :: RINGCAT1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y1, y2 being set st GO x,y1 & GO x,y2 holds
y1 = y2
proof end;

theorem Th21: :: RINGCAT1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe ex x being set st
( x in UN & GO x, Z3 )
proof end;

definition
let UN be Universe;
func RingObjects UN -> set means :Def17: :: RINGCAT1:def 17
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 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 end;
end;

:: deftheorem Def17 defines RingObjects RINGCAT1:def 17 :
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 Th22: :: RINGCAT1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe holds Z3 in RingObjects UN
proof end;

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

theorem Th23: :: RINGCAT1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for x being Element of RingObjects UN holds x is strict Ring
proof end;

registration
let UN be Universe;
cluster RingObjects UN -> non empty Ring_DOMAIN-like ;
coherence
RingObjects UN is Ring_DOMAIN-like
proof end;
end;

definition
let V be Ring_DOMAIN;
func Morphs V -> RingMorphism_DOMAIN means :Def18: :: RINGCAT1:def 18
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 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 end;
end;

:: deftheorem Def18 defines Morphs RINGCAT1:def 18 :
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 end;
:: original: cod
redefine func cod F -> Element of V;
coherence
cod F is Element of V
proof 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 19
ID G;
coherence
ID G is strict Element of Morphs V
by Def18;
end;

:: deftheorem defines ID RINGCAT1:def 19 :
for V being Ring_DOMAIN
for G being Element of V holds ID G = ID G;

definition
let V be Ring_DOMAIN;
func dom V -> Function of Morphs V,V means :Def20: :: 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 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 end;
func cod V -> Function of Morphs V,V means :Def21: :: 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 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 end;
func ID V -> Function of V, Morphs V means :Def22: :: RINGCAT1:def 22
for G being Element of V holds it . G = ID G;
existence
ex b1 being Function of V, Morphs V st
for G being Element of V holds b1 . G = ID G
proof end;
uniqueness
for b1, b2 being Function of V, Morphs V st ( for G being Element of V holds b1 . G = ID G ) & ( for G being Element of V holds b2 . G = ID G ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 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 Def21 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 Def22 defines ID RINGCAT1:def 22 :
for V being Ring_DOMAIN
for b2 being Function of V, Morphs V holds
( b2 = ID V iff for G being Element of V holds b2 . G = ID G );

theorem Th24: :: RINGCAT1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th25: :: RINGCAT1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let V be Ring_DOMAIN;
func comp V -> PartFunc of [:(Morphs V),(Morphs V):], Morphs V means :Def23: :: 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 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 end;
end;

:: deftheorem Def23 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)),(ID (RingObjects UN)) #);
coherence
CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)),(ID (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)),(ID (RingObjects UN)) #);

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

theorem Th26: :: RINGCAT1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th27: :: RINGCAT1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for f being Morphism of (RingCat UN)
for f' being Element of Morphs (RingObjects UN)
for b being Object of (RingCat UN)
for b' being Element of RingObjects UN holds
( f is strict Element of Morphs (RingObjects UN) & f' is Morphism of (RingCat UN) & b is strict Element of RingObjects UN & b' is Object of (RingCat UN) )
proof end;

theorem Th28: :: RINGCAT1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for b being Object of (RingCat UN)
for b' being Element of RingObjects UN st b = b' holds
id b = ID b'
proof end;

theorem Th29: :: RINGCAT1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for f being Morphism of (RingCat UN)
for f' being Element of Morphs (RingObjects UN) st f = f' holds
( dom f = dom f' & cod f = cod f' )
proof end;

theorem Th30: :: RINGCAT1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for UN being Universe
for f, g being Morphism of (RingCat UN)
for f', g' being Element of Morphs (RingObjects UN) st f = f' & g = g' holds
( ( dom g = cod f implies dom g' = cod f' ) & ( dom g' = cod f' implies dom g = cod f ) & ( dom g = cod f implies [g',f'] in dom (comp (RingObjects UN)) ) & ( [g',f'] in dom (comp (RingObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g * f = g' * f' ) & ( dom f = dom g implies dom f' = dom g' ) & ( dom f' = dom g' implies dom f = dom g ) & ( cod f = cod g implies cod f' = cod g' ) & ( cod f' = cod g' implies cod f = cod g ) )
proof 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 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 end;

Lm11: for UN being Universe
for b being Object of (RingCat UN) holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of (RingCat UN) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (RingCat UN) st dom g = b holds
g * (id b) = g ) )
proof end;

registration
let UN be Universe;
cluster RingCat UN -> strict Category-like ;
coherence
RingCat UN is Category-like
proof end;
end;