let UN be Universe; :: thesis: for R being Ring
for f, g being Morphism of (LModCat (UN,R))
for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
let R be Ring; :: thesis: for f, g being Morphism of (LModCat (UN,R))
for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 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 (LModCat (UN,R)); :: thesis: for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
let f9, g9 be Element of Morphs (LModObjects (UN,R)); :: thesis: ( f = f9 & g = g9 implies ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) )
assume that
A1: f = f9 and
A2: g = g9 ; :: thesis: ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
A3: cod f = cod f9 by A1, Th13;
hence ( dom g = cod f iff dom g9 = cod f9 ) by A2, Th13; :: thesis: ( ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
dom g = dom g9 by A2, Th13;
hence A4: ( dom g = cod f iff [g9,f9] in dom (comp (LModObjects (UN,R))) ) by A3, Th11; :: thesis: ( ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
thus ( dom g = cod f implies g (*) f = g9 * f9 ) :: thesis: ( ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) dom f = dom f9 by A1, Th13;
hence ( dom f = dom g iff dom f9 = dom g9 ) by A2, Th13; :: thesis: ( cod f = cod g iff cod f9 = cod g9 )
cod g = cod g9 by A2, Th13;
hence ( cod f = cod g iff cod f9 = cod g9 ) by A1, Th13; :: thesis: verum