let UN be Universe; :: thesis: for R being Ring
for f being Morphism of (LModCat UN,R)
for f' being Element of Morphs (LModObjects UN,R) st f = f' holds
( dom f = dom f' & cod f = cod f' )
let R be Ring; :: thesis: for f being Morphism of (LModCat UN,R)
for f' being Element of Morphs (LModObjects UN,R) st f = f' holds
( dom f = dom f' & cod f = cod f' )
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 f' being Element of Morphs (LModObjects UN,R) st f = f' holds
( dom f = dom f' & cod f = cod f' )
let f' be Element of Morphs (LModObjects UN,R); :: thesis: ( f = f' implies ( dom f = dom f' & cod f = cod f' ) )
assume A1: f = f' ; :: thesis: ( dom f = dom f' & cod f = cod f' )
hence dom f = dom' f' by Def11
.= dom f' ;
:: thesis: cod f = cod f'
thus cod f = cod' f' by Def12, A1
.= cod f' ; :: thesis: verum