let UN be Universe; :: thesis: for f, g being Morphism of (RingCat UN)
for f', g' being Element of Morphs (RingObjects 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 (RingObjects UN)) ) & ( [g',f'] in dom (comp (RingObjects 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 = RingCat UN;
set V = RingObjects UN;
set X = Morphs (RingObjects UN);
let f, g be Morphism of (RingCat UN); :: thesis: for f', g' being Element of Morphs (RingObjects 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 (RingObjects UN)) ) & ( [g',f'] in dom (comp (RingObjects 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 (RingObjects 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 (RingObjects UN)) ) & ( [g',f'] in dom (comp (RingObjects 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 (RingObjects UN)) ) & ( [g',f'] in dom (comp (RingObjects 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 Def20;
A3: cod f = cod f' by A1, Def21;
A4: dom f = dom f' by A1, Def20;
A5: cod g = cod g' by A1, Def21;
thus ( dom g = cod f iff dom g' = cod f' ) by A1, A3, Def20; :: thesis: ( ( dom g = cod f implies [g',f'] in dom (comp (RingObjects UN)) ) & ( [g',f'] in dom (comp (RingObjects 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 (RingObjects UN)) ) by A2, A3, Def23; :: 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 (RingCat UN) by Th26;
hence g * f = (comp (RingObjects UN)) . g',f' by A1, CAT_1:def 4
.= g' * f' by A6, A7, Def23 ;
:: thesis: verum

end;

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