let UN be Universe; :: thesis: for f, g being Morphism of holds
( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f )
set C = RingCat UN;
set V = RingObjects UN;
let f, g be Morphism of ; :: thesis: ( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f )
reconsider f' = f as Element of Morphs (RingObjects UN) ;
reconsider g' = g as Element of Morphs (RingObjects UN) ;
( dom g = dom g' & cod f = cod f' ) by Def20, Def21;
hence ( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f ) by Def23; :: thesis: verum