let UN be Universe; :: thesis: for R being Ring
for f, g being Morphism of (LModCat (UN,R)) holds
( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f )
let R be Ring; :: thesis: for f, g being Morphism of (LModCat (UN,R)) holds
( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f )
set C = LModCat (UN,R);
set V = LModObjects (UN,R);
let f, g be Morphism of (LModCat (UN,R)); :: thesis: ( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f )
reconsider f9 = f as Element of Morphs (LModObjects (UN,R)) ;
reconsider g9 = g as Element of Morphs (LModObjects (UN,R)) ;
A1: cod f = cod' f9 by Def12
.= cod f9 ;
A2: dom g = dom' g9 by Def11
.= dom g9 ;

A3: now :: thesis: ( dom g = cod f implies [g,f] in dom the Comp of (LModCat (UN,R)) )

assume dom g = cod f ; :: thesis: [g,f] in dom the Comp of (LModCat (UN,R))
then dom' g9 = cod' f9 by A2, A1;
hence [g,f] in dom the Comp of (LModCat (UN,R)) by Def13; :: thesis: verum

end;

now :: thesis: ( [g,f] in dom the Comp of (LModCat (UN,R)) implies dom g = cod f )

assume [g,f] in dom the Comp of (LModCat (UN,R)) ; :: thesis: dom g = cod f
then dom' g9 = cod' f9 by Def13
.= cod f9 ;
hence dom g = cod f by A2, A1; :: thesis: verum

end;

hence ( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f ) by A3; :: thesis: verum