let UN be Universe; :: thesis: for f, g being Morphism of
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 ; :: 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 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 (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 ) )
A3: cod f = cod f' by A1, Def33;
hence ( dom g = cod f iff dom g' = cod f' ) by A2, 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 ) )
dom g = dom g' by A2, Def32;
hence A4: ( dom g = cod f iff [g',f'] in dom (comp (GroupObjects UN)) ) by 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 A5: 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, A2, CAT_1:def 4
.= g' * f' by A4, A5, Def35 ;
:: thesis: verum

end;

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