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 f' = f as Element of Morphs (LModObjects UN,R) ;
reconsider g' = g as Element of Morphs (LModObjects UN,R) ;
A1: dom g = dom' g' by Def11
.= dom g' ;
A2: cod f = cod' f' by Def12
.= cod f' ;

A3: now

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

end;

now

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

end;

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