set C = GroupCat UN;
set X = Morphs (GroupObjects UN);
thus GroupCat UN is transitive :: thesis: ( GroupCat UN is associative & GroupCat UN is with_identities )
proof
let f, g be Morphism of (GroupCat UN); :: according to CAT_1:def 7 :: thesis: ( not dom g = cod f or ( 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
end;
thus GroupCat UN is associative :: thesis: GroupCat UN is with_identities
proof
let f, g, h be Morphism of (GroupCat UN); :: according to CAT_1:def 8 :: thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
assume A4: ( dom h = cod g & dom g = cod f ) ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f
reconsider f9 = f, g9 = g, h9 = h as strict Element of Morphs (GroupObjects UN) by Th34;
A5: ( h9 * g9 = h (*) g & dom (h (*) g) = cod f ) by A4, Lm1, Th35;
A6: ( dom h9 = cod g9 & dom g9 = cod f9 ) by A4, Th35;
then reconsider gf = g9 * f9, hg = h9 * g9 as Element of Morphs (GroupObjects UN) by Th32;
( g9 * f9 = g (*) f & dom h = cod (g (*) f) ) by A4, Lm1, Th35;
then h (*) (g (*) f) = h9 * gf by Th35
.= hg * f9 by A6, Th22
.= (h (*) g) (*) f by A5, Th35 ;
hence h (*) (g (*) f) = (h (*) g) (*) f ; :: thesis: verum
end;
thus GroupCat UN is with_identities :: thesis: verum
proof
let a be Element of (GroupCat UN); :: according to CAT_1:def 10 :: thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of (GroupCat UN) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider aa = a as Element of GroupObjects UN ;
reconsider ii = ID aa as Morphism of (GroupCat UN) ;
reconsider ia = ii as GroupMorphismStr ;
A7: dom ii = dom ia by Def25
.= a ;
cod ii = cod ia by Def26
.= a ;
then reconsider ii = ii as Morphism of a,a by A7, CAT_1:4;
take ii ; :: thesis: for b1 being Element of the carrier of (GroupCat UN) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
thus for b1 being Element of the carrier of (GroupCat UN) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) by Lm2; :: thesis: verum
end;