let UN be Universe; :: thesis: for R being Ring
for f being Morphism of (LModCat (UN,R))
for f9 being Element of Morphs (LModObjects (UN,R)) st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
let R be Ring; :: thesis: for f being Morphism of (LModCat (UN,R))
for f9 being Element of Morphs (LModObjects (UN,R)) st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
set C = LModCat (UN,R);
set V = LModObjects (UN,R);
set X = Morphs (LModObjects (UN,R));
let f be Morphism of (LModCat (UN,R)); :: thesis: for f9 being Element of Morphs (LModObjects (UN,R)) st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
let f9 be Element of Morphs (LModObjects (UN,R)); :: thesis: ( f = f9 implies ( dom f = dom f9 & cod f = cod f9 ) )
assume A1: f = f9 ; :: thesis: ( dom f = dom f9 & cod f = cod f9 )
hence dom f = dom' f9 by Def11
.= dom f9 ;
:: thesis: cod f = cod f9
thus cod f = cod' f9 by A1, Def12
.= cod f9 ; :: thesis: verum