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