let UN be Universe; :: thesis: for f, g being Morphism of (RingCat UN) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
set X = Morphs (RingObjects UN);
let f, g be Morphism of (RingCat UN); :: thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
assume A1: dom g = cod f ; :: thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
reconsider g9 = g as strict Element of Morphs (RingObjects UN) by Th22;
reconsider f9 = f as strict Element of Morphs (RingObjects UN) by Th22;
A2: dom g9 = cod f9 by A1, Th23;
then reconsider gf = g9 * f9 as Element of Morphs (RingObjects UN) by Th20;
A3: gf = g (*) f by A1, Th23;
( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by A2, Th8;
hence ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, Th23; :: thesis: verum