let UN be Universe; :: thesis: for R being Ring
for f, g being Morphism of
for f', g' being Element of Morphs (LModObjects UN,R) st f = f' & g = g' holds
( ( dom g = cod f implies dom g' = cod f' ) & ( dom g' = cod f' implies dom g = cod f ) & ( dom g = cod f implies [g',f'] in dom (comp (LModObjects UN,R)) ) & ( [g',f'] in dom (comp (LModObjects UN,R)) implies dom g = cod f ) & ( dom g = cod f implies g * f = g' * f' ) & ( dom f = dom g implies dom f' = dom g' ) & ( dom f' = dom g' implies dom f = dom g ) & ( cod f = cod g implies cod f' = cod g' ) & ( cod f' = cod g' implies cod f = cod g ) )
let R be Ring; :: thesis: for f, g being Morphism of
for f', g' being Element of Morphs (LModObjects UN,R) st f = f' & g = g' holds
( ( dom g = cod f implies dom g' = cod f' ) & ( dom g' = cod f' implies dom g = cod f ) & ( dom g = cod f implies [g',f'] in dom (comp (LModObjects UN,R)) ) & ( [g',f'] in dom (comp (LModObjects UN,R)) implies dom g = cod f ) & ( dom g = cod f implies g * f = g' * f' ) & ( dom f = dom g implies dom f' = dom g' ) & ( dom f' = dom g' implies dom f = dom g ) & ( cod f = cod g implies cod f' = cod g' ) & ( cod f' = cod g' implies cod f = cod g ) )
set C = LModCat UN,R;
set V = LModObjects UN,R;
set X = Morphs (LModObjects UN,R);
let f, g be Morphism of ; :: thesis: for f', g' being Element of Morphs (LModObjects UN,R) st f = f' & g = g' holds
( ( dom g = cod f implies dom g' = cod f' ) & ( dom g' = cod f' implies dom g = cod f ) & ( dom g = cod f implies [g',f'] in dom (comp (LModObjects UN,R)) ) & ( [g',f'] in dom (comp (LModObjects UN,R)) implies dom g = cod f ) & ( dom g = cod f implies g * f = g' * f' ) & ( dom f = dom g implies dom f' = dom g' ) & ( dom f' = dom g' implies dom f = dom g ) & ( cod f = cod g implies cod f' = cod g' ) & ( cod f' = cod g' implies cod f = cod g ) )
let f', g' be Element of Morphs (LModObjects UN,R); :: thesis: ( f = f' & g = g' implies ( ( dom g = cod f implies dom g' = cod f' ) & ( dom g' = cod f' implies dom g = cod f ) & ( dom g = cod f implies [g',f'] in dom (comp (LModObjects UN,R)) ) & ( [g',f'] in dom (comp (LModObjects UN,R)) implies dom g = cod f ) & ( dom g = cod f implies g * f = g' * f' ) & ( dom f = dom g implies dom f' = dom g' ) & ( dom f' = dom g' implies dom f = dom g ) & ( cod f = cod g implies cod f' = cod g' ) & ( cod f' = cod g' implies cod f = cod g ) ) )
assume that
A1: f = f' and
A2: g = g' ; :: thesis: ( ( dom g = cod f implies dom g' = cod f' ) & ( dom g' = cod f' implies dom g = cod f ) & ( dom g = cod f implies [g',f'] in dom (comp (LModObjects UN,R)) ) & ( [g',f'] in dom (comp (LModObjects UN,R)) implies dom g = cod f ) & ( dom g = cod f implies g * f = g' * f' ) & ( dom f = dom g implies dom f' = dom g' ) & ( dom f' = dom g' implies dom f = dom g ) & ( cod f = cod g implies cod f' = cod g' ) & ( cod f' = cod g' implies cod f = cod g ) )
A3: cod f = cod f' by A1, Th17;
hence ( dom g = cod f iff dom g' = cod f' ) by A2, Th17; :: thesis: ( ( dom g = cod f implies [g',f'] in dom (comp (LModObjects UN,R)) ) & ( [g',f'] in dom (comp (LModObjects UN,R)) implies dom g = cod f ) & ( dom g = cod f implies g * f = g' * f' ) & ( dom f = dom g implies dom f' = dom g' ) & ( dom f' = dom g' implies dom f = dom g ) & ( cod f = cod g implies cod f' = cod g' ) & ( cod f' = cod g' implies cod f = cod g ) )
dom g = dom g' by A2, Th17;
hence A4: ( dom g = cod f iff [g',f'] in dom (comp (LModObjects UN,R)) ) by A3, Th13; :: thesis: ( ( dom g = cod f implies g * f = g' * f' ) & ( dom f = dom g implies dom f' = dom g' ) & ( dom f' = dom g' implies dom f = dom g ) & ( cod f = cod g implies cod f' = cod g' ) & ( cod f' = cod g' implies cod f = cod g ) )
thus ( dom g = cod f implies g * f = g' * f' ) :: thesis: ( ( dom f = dom g implies dom f' = dom g' ) & ( dom f' = dom g' implies dom f = dom g ) & ( cod f = cod g implies cod f' = cod g' ) & ( cod f' = cod g' implies cod f = cod g ) )

proof

assume A5: dom g = cod f ; :: thesis: g * f = g' * f'
then [g,f] in dom the Comp of (LModCat UN,R) by Th14;
hence g * f = (comp (LModObjects UN,R)) . g',f' by A1, A2, CAT_1:def 4
.= g' * f' by A4, A5, Def14 ;
:: thesis: verum

end;

dom f = dom f' by A1, Th17;
hence ( dom f = dom g iff dom f' = dom g' ) by A2, Th17; :: thesis: ( cod f = cod g iff cod f' = cod g' )
cod g = cod g' by A2, Th17;
hence ( cod f = cod g iff cod f' = cod g' ) by A1, Th17; :: thesis: verum