let UN be Universe; :: thesis: for f, g being Morphism of (GroupCat UN) holds
( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f )
set C = GroupCat UN;
set V = GroupObjects UN;
let f, g be Morphism of (GroupCat UN); :: thesis: ( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f )
reconsider f9 = f as Element of Morphs (GroupObjects UN) ;
reconsider g9 = g as Element of Morphs (GroupObjects UN) ;
( dom g = dom g9 & cod f = cod f9 ) by Def25, Def26;
hence ( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f ) by Def27; :: thesis: verum