let UN be Universe; :: thesis: for f, g being Morphism of 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 ; :: 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 g' = g as strict Element of Morphs (RingObjects UN) by Th27;
reconsider f' = f as strict Element of Morphs (RingObjects UN) by Th27;
A2: dom g' = cod f' by A1, Th30;
then reconsider gf = g' * f' as Element of Morphs (RingObjects UN) by Th25;
A3: gf = g * f by A1, Th30;
( dom (g' * f') = dom f' & cod (g' * f') = cod g' ) by A2, Th11;
hence ( dom (g * f) = dom f & cod (g * f) = cod g ) by A3, Th30; :: thesis: verum