let UN be Universe; :: thesis: for f, g being Morphism of (RingCat UN) 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 (RingCat UN); :: thesis: ( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f )
reconsider f9 = f as Element of Morphs (RingObjects UN) ;
reconsider g9 = g as Element of Morphs (RingObjects UN) ;
( dom g = dom g9 & cod f = cod f9 ) by Def19, Def20;
hence ( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f ) by Def21; :: thesis: verum