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 Th47;
reconsider f9 = f as strict Element of Morphs (GroupObjects UN) by Th47;
A2: dom g9 = cod f9 by A1, Th50;
then reconsider gf = g9 * f9 as Element of Morphs (GroupObjects UN) by Th45;
A3: gf = g * f by A1, Th50;
( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by A2, Th31;
hence ( dom (g * f) = dom f & cod (g * f) = cod g ) by A3, Th50; :: thesis: verum