let UN be Universe; :: thesis: for R being Ring
for b being Object of (LModCat (UN,R)) holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of (LModCat (UN,R)) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (LModCat (UN,R)) st dom g = b holds
g * (id b) = g ) )
let R be Ring; :: thesis: for b being Object of (LModCat (UN,R)) holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of (LModCat (UN,R)) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (LModCat (UN,R)) st dom g = b holds
g * (id b) = g ) )
set C = LModCat (UN,R);
set V = LModObjects (UN,R);
set X = Morphs (LModObjects (UN,R));
let b be Object of (LModCat (UN,R)); :: thesis: ( dom (id b) = b & cod (id b) = b & ( for f being Morphism of (LModCat (UN,R)) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (LModCat (UN,R)) st dom g = b holds
g * (id b) = g ) )
reconsider b9 = b as Element of LModObjects (UN,R) ;
reconsider b99 = b9 as LeftMod of R ;
A1: id b = ID b9 by Th16;
hence A2: dom (id b) = dom (ID b99) by Th17
.= b by MOD_2:26 ;
:: thesis: ( cod (id b) = b & ( for f being Morphism of (LModCat (UN,R)) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (LModCat (UN,R)) st dom g = b holds
g * (id b) = g ) )
thus A3: cod (id b) = cod (ID b99) by A1, Th17
.= b by MOD_2:26 ; :: thesis: ( ( for f being Morphism of (LModCat (UN,R)) st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of (LModCat (UN,R)) st dom g = b holds
g * (id b) = g ) )
thus for f being Morphism of (LModCat (UN,R)) st cod f = b holds
(id b) * f = f :: thesis: for g being Morphism of (LModCat (UN,R)) st dom g = b holds
g * (id b) = g

proof

let f be Morphism of (LModCat (UN,R)); :: thesis: ( cod f = b implies (id b) * f = f )
assume A4: cod f = b ; :: thesis: (id b) * f = f
reconsider f1 = f as Element of Morphs (LModObjects (UN,R)) ;
ex G, H being strict Element of LModObjects (UN,R) st f1 is strict Morphism of G,H by Def7;
then reconsider f9 = f1 as strict LModMorphism of R ;
A5: cod f9 = b99 by A4, Th17;
thus (id b) * f = (ID b99) * f9 by A1, A2, A4, Th18
.= f by A5, MOD_2:26 ; :: thesis: verum

end;

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

proof

let f be Morphism of (LModCat (UN,R)); :: thesis: ( dom f = b implies f * (id b) = f )
assume A6: dom f = b ; :: thesis: f * (id b) = f
reconsider f1 = f as Element of Morphs (LModObjects (UN,R)) ;
ex G, H being strict Element of LModObjects (UN,R) st f1 is strict Morphism of G,H by Def7;
then reconsider f9 = f1 as strict LModMorphism of R ;
A7: dom f9 = b99 by A6, Th17;
thus f * (id b) = f9 * (ID b99) by A1, A3, A6, Th18
.= f by A7, MOD_2:26 ; :: thesis: verum

end;