let UN be Universe; :: thesis: for R being Ring
for b being Object of (LModCat (UN,R))
for b9 being Element of LModObjects (UN,R) st b = b9 holds
id b = ID b9
let R be Ring; :: thesis: for b being Object of (LModCat (UN,R))
for b9 being Element of LModObjects (UN,R) st b = b9 holds
id b = ID b9
set C = LModCat (UN,R);
set V = LModObjects (UN,R);
let b be Object of (LModCat (UN,R)); :: thesis: for b9 being Element of LModObjects (UN,R) st b = b9 holds
id b = ID b9
let b9 be Element of LModObjects (UN,R); :: thesis: ( b = b9 implies id b = ID b9 )
assume b = b9 ; :: thesis: id b = ID b9
hence id b = (ID (LModObjects (UN,R))) . b9 by CAT_1:def 5
.= ID b9 by Def13 ;
:: thesis: verum