let UN be Universe; :: thesis: for f, g being Morphism of (GroupCat UN) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
set X = Morphs (GroupObjects UN);
let f, g be Morphism of (GroupCat 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 (GroupObjects UN) by Th34;
reconsider f9 = f as strict Element of Morphs (GroupObjects UN) by Th34;
A2: dom g9 = cod f9 by A1, Th35;
then reconsider gf = g9 * f9 as Element of Morphs (GroupObjects UN) by Th32;
A3: gf = g (*) f by A1, Th35;
( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by A2, Th20;
hence ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, Th35; :: thesis: verum