let UN be Universe; :: thesis: 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 ) )
set C = RingCat UN;
set V = RingObjects UN;
set X = Morphs (RingObjects UN);
let b be Object of (RingCat UN); :: thesis: ( 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 ) )
reconsider b9 = b as Element of RingObjects UN ;
reconsider b99 = b9 as Ring ;
A1: id b = ID b9 by Th28;
hence A2: dom (id b) = dom (ID b99) by Def20
.= b ;
:: thesis: ( 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 ) )
thus A3: cod (id b) = cod (ID b99) by A1, Def21
.= b ; :: thesis: ( ( 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 ) )
thus for f being Morphism of (RingCat UN) st cod f = b holds
(id b) * f = f :: thesis: for g being Morphism of (RingCat UN) st dom g = b holds
g * (id b) = g

proof

let f be Morphism of (RingCat UN); :: thesis: ( cod f = b implies (id b) * f = f )
assume A4: cod f = b ; :: thesis: (id b) * f = f
reconsider f1 = f as strict Element of Morphs (RingObjects UN) by Th27;
reconsider f9 = f1 as strict RingMorphism ;
A5: cod f9 = b99 by A4, Def21;
thus (id b) * f = (ID b99) * f9 by A1, A2, A4, Th30
.= f by A5, Th14 ; :: thesis: verum

end;

thus for g being Morphism of (RingCat UN) st dom g = b holds
g * (id b) = g :: thesis: verum

proof

let f be Morphism of (RingCat UN); :: thesis: ( dom f = b implies f * (id b) = f )
assume A6: dom f = b ; :: thesis: f * (id b) = f
reconsider f1 = f as strict Element of Morphs (RingObjects UN) by Th27;
reconsider f9 = f1 as strict RingMorphism ;
A7: dom f9 = b99 by A6, Def20;
thus f * (id b) = f9 * (ID b99) by A1, A3, A6, Th30
.= f by A7, Th14 ; :: thesis: verum

end;