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

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 Def14; :: thesis: verum

end;

now

assume [g,f] in dom the Comp of (LModCat UN,R) ; :: thesis: dom g = cod f
then dom' g9 = cod' f9 by Def14
.= 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