let UN be Universe; :: thesis: for f, g being Morphism of (GroupCat UN)
for f9, g9 being Element of Morphs (GroupObjects UN) 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 (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) 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 = GroupCat UN;
set V = GroupObjects UN;
set X = Morphs (GroupObjects UN);
let f, g be Morphism of (GroupCat UN); :: thesis: for f9, g9 being Element of Morphs (GroupObjects UN) 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 (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) 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 (GroupObjects UN); :: 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 (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) 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 (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) 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, Def26;
hence ( dom g = cod f iff dom g9 = cod f9 ) by A2, Def25; :: thesis: ( ( dom g = cod f implies [g9,f9] in dom (comp (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) 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, Def25;
hence A4: ( dom g = cod f iff [g9,f9] in dom (comp (GroupObjects UN)) ) by A3, Def27; :: 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 ) )

proof

assume A5: dom g = cod f ; :: thesis: g (*) f = g9 * f9
then [g,f] in dom the Comp of (GroupCat UN) by Th33;
hence g (*) f = (comp (GroupObjects UN)) . (g9,f9) by A1, A2, CAT_1:def 1
.= g9 * f9 by A4, A5, Def27 ;
:: thesis: verum

end;

dom f = dom f9 by A1, Def25;
hence ( dom f = dom g iff dom f9 = dom g9 ) by A2, Def25; :: thesis: ( cod f = cod g iff cod f9 = cod g9 )
cod g = cod g9 by A2, Def26;
hence ( cod f = cod g iff cod f9 = cod g9 ) by A1, Def26; :: thesis: verum