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