let UN be Universe; :: thesis: for f, g being Morphism of (GroupCat UN)
for f', g' being Element of Morphs (GroupObjects UN) 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 (GroupObjects UN)) ) & ( [g',f'] in dom (comp (GroupObjects UN)) 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 = GroupCat UN;
set V = GroupObjects UN;
set X = Morphs (GroupObjects UN);
let f, g be Morphism of (GroupCat UN); :: thesis: for f', g' being Element of Morphs (GroupObjects UN) 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 (GroupObjects UN)) ) & ( [g',f'] in dom (comp (GroupObjects UN)) 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 (GroupObjects UN); :: 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 (GroupObjects UN)) ) & ( [g',f'] in dom (comp (GroupObjects UN)) 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 A1: ( f = f' & 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 (GroupObjects UN)) ) & ( [g',f'] in dom (comp (GroupObjects UN)) 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 ) )
then A2: dom g = dom g' by Def32;
A3: cod f = cod f' by A1, Def33;
A4: dom f = dom f' by A1, Def32;
A5: cod g = cod g' by A1, Def33;
thus ( dom g = cod f iff dom g' = cod f' ) by A1, A3, Def32; :: thesis: ( ( dom g = cod f implies [g',f'] in dom (comp (GroupObjects UN)) ) & ( [g',f'] in dom (comp (GroupObjects UN)) 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 ) )
thus A6: ( dom g = cod f iff [g',f'] in dom (comp (GroupObjects UN)) ) by A2, A3, Def35; :: 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 A7: dom g = cod f ; :: thesis: g * f = g' * f'
then [g,f] in dom the Comp of (GroupCat UN) by Th46;
hence g * f = (comp (GroupObjects UN)) . g',f' by A1, CAT_1:def 4
.= g' * f' by A6, A7, Def35 ;
:: thesis: verum

end;

thus ( dom f = dom g iff dom f' = dom g' ) by A1, A4, Def32; :: thesis: ( cod f = cod g iff cod f' = cod g' )
thus ( cod f = cod g iff cod f' = cod g' ) by A1, A5, Def33; :: thesis: verum