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 b' = b as Element of RingObjects UN ;
reconsider b'' = b' as Ring ;
A1: id b = ID b' by Th28;
hence A2: dom (id b) = dom (ID b'') 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 b'') 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 f' = f1 as strict RingMorphism ;
A5: cod f' = b'' by A4, Def21;
thus (id b) * f = (ID b'') * f' 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 f' = f1 as strict RingMorphism ;
A7: dom f' = b'' by A6, Def20;
thus f * (id b) = f' * (ID b'') by A1, A3, A6, Th30
.= f by A7, Th14 ; :: thesis: verum

end;