let C be Category; :: thesis: CategoryStr(# the carrier' of C, the Comp of C #) is category
consider o being object such that
A1: o in the carrier of C by XBOOLE_0:def 1;
reconsider o = o as Object of C by A1;
reconsider cc = CategoryStr(# the carrier' of C, the Comp of C #) as non empty CategoryStr ;
A2: for f, g being morphism of cc
for f1, g1 being Element of the carrier' of C st g = g1 & f = f1 & g |> f holds
g (*) f = g1 (*) f1

proof

let f, g be morphism of cc; :: thesis: for f1, g1 being Element of the carrier' of C st g = g1 & f = f1 & g |> f holds
g (*) f = g1 (*) f1
let f1, g1 be Element of the carrier' of C; :: thesis: ( g = g1 & f = f1 & g |> f implies g (*) f = g1 (*) f1 )
assume A3: ( g = g1 & f = f1 ) ; :: thesis: ( not g |> f or g (*) f = g1 (*) f1 )
assume A4: g |> f ; :: thesis: g (*) f = g1 (*) f1
thus g (*) f = (CompMap cc) . [g1,f1] by A3, A4, Lm4
.= the Comp of C . (g1,f1) by BINOP_1:def 1
.= g1 (*) f1 by A3, A4, CAT_1:def 1 ; :: thesis: verum

end;

A5: for f, g, h being morphism of cc holds
( ( h (*) g |> f & h |> g implies g |> f ) & ( h |> g (*) f & g |> f implies h |> g ) & ( g |> f & h |> g implies ( h (*) g |> f & h |> g (*) f ) ) )

proof

let f, g, h be morphism of cc; :: thesis: ( ( h (*) g |> f & h |> g implies g |> f ) & ( h |> g (*) f & g |> f implies h |> g ) & ( g |> f & h |> g implies ( h (*) g |> f & h |> g (*) f ) ) )
reconsider f1 = f, g1 = g, h1 = h as Morphism of C ;
thus ( h (*) g |> f & h |> g implies g |> f ) :: thesis: ( ( h |> g (*) f & g |> f implies h |> g ) & ( g |> f & h |> g implies ( h (*) g |> f & h |> g (*) f ) ) )

proof

assume A6: h (*) g |> f ; :: thesis: ( not h |> g or g |> f )
assume A7: h |> g ; :: thesis: g |> f
then A8: dom h1 = cod g1 by CAT_1:def 6;
h (*) g = h1 (*) g1 by A7, A2;
then dom (h1 (*) g1) = cod f1 by A6, CAT_1:def 6;
then dom g1 = cod f1 by A8, CAT_1:def 7;
hence g |> f by CAT_1:def 6; :: thesis: verum

end;

thus ( h |> g (*) f & g |> f implies h |> g ) :: thesis: ( g |> f & h |> g implies ( h (*) g |> f & h |> g (*) f ) )

proof

assume A9: h |> g (*) f ; :: thesis: ( not g |> f or h |> g )
assume A10: g |> f ; :: thesis: h |> g
then A11: dom g1 = cod f1 by CAT_1:def 6;
g (*) f = g1 (*) f1 by A10, A2;
then dom h1 = cod (g1 (*) f1) by A9, CAT_1:def 6;
then dom h1 = cod g1 by A11, CAT_1:def 7;
hence h |> g by CAT_1:def 6; :: thesis: verum

end;

assume A12: g |> f ; :: thesis: ( not h |> g or ( h (*) g |> f & h |> g (*) f ) )
then A13: dom g1 = cod f1 by CAT_1:def 6;
assume A14: h |> g ; :: thesis: ( h (*) g |> f & h |> g (*) f )
A15: dom h1 = cod g1 by A14, CAT_1:def 6;
dom (h1 (*) g1) = cod f1 by A13, A15, CAT_1:def 7;
then [(h1 (*) g1),f1] in dom (CompMap cc) by CAT_1:def 6;
hence h (*) g |> f by A14, A2; :: thesis: h |> g (*) f
dom h1 = cod g1 by A14, CAT_1:def 6;
then dom h1 = cod (g1 (*) f1) by A13, CAT_1:def 7;
then [h1,(g1 (*) f1)] in dom (CompMap cc) by CAT_1:def 6;
hence h |> g (*) f by A12, A2; :: thesis: verum

end;

A16: for f, g, h being morphism of cc st h |> g & g |> f holds
h (*) (g (*) f) = (h (*) g) (*) f

proof

let f, g, h be morphism of cc; :: thesis: ( h |> g & g |> f implies h (*) (g (*) f) = (h (*) g) (*) f )
reconsider f1 = f, g1 = g, h1 = h, gf1 = g (*) f, hg1 = h (*) g as Morphism of C ;
assume A17: h |> g ; :: thesis: ( not g |> f or h (*) (g (*) f) = (h (*) g) (*) f )
then A18: dom h1 = cod g1 by CAT_1:def 6;
assume A19: g |> f ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f
then A20: dom g1 = cod f1 by CAT_1:def 6;
A21: h |> g (*) f by A17, A19, A5;
A22: h (*) g |> f by A17, A19, A5;
thus h (*) (g (*) f) = h1 (*) gf1 by A21, A2
.= h1 (*) (g1 (*) f1) by A19, A2
.= (h1 (*) g1) (*) f1 by A20, A18, CAT_1:def 8
.= hg1 (*) f1 by A17, A2
.= (h (*) g) (*) f by A22, A2 ; :: thesis: verum

end;

A23: for f being morphism of cc st f in Mor cc holds
( ex c being morphism of cc st
( c |> f & c is identity ) & ex d being morphism of cc st
( f |> d & d is identity ) )

proof

let f be morphism of cc; :: thesis: ( f in Mor cc implies ( ex c being morphism of cc st
( c |> f & c is identity ) & ex d being morphism of cc st
( f |> d & d is identity ) ) )
assume f in Mor cc ; :: thesis: ( ex c being morphism of cc st
( c |> f & c is identity ) & ex d being morphism of cc st
( f |> d & d is identity ) )
reconsider f1 = f as Morphism of C ;
thus ex c being morphism of cc st
( c |> f & c is identity ) :: thesis: ex d being morphism of cc st
( f |> d & d is identity )

proof

set c1 = id (cod f1);
A24: dom (id (cod f1)) = cod f1 ;
reconsider c = id (cod f1) as morphism of cc ;
take c ; :: thesis: ( c |> f & c is identity )
thus c |> f by A24, CAT_1:def 6; :: thesis: c is identity
A25: for ff being morphism of cc st c |> ff holds
c (*) ff = ff

proof

let ff be morphism of cc; :: thesis: ( c |> ff implies c (*) ff = ff )
reconsider ff1 = ff as Morphism of C ;
assume A26: c |> ff ; :: thesis: c (*) ff = ff
then A27: dom (id (cod f1)) = cod ff1 by CAT_1:def 6;
thus c (*) ff = (id (cod f1)) (*) ff1 by A26, A2
.= ff by A27, CAT_1:21 ; :: thesis: verum

end;

for gg being morphism of cc st gg |> c holds
gg (*) c = gg

proof

let gg be morphism of cc; :: thesis: ( gg |> c implies gg (*) c = gg )
reconsider gg1 = gg as Morphism of C ;
assume A28: gg |> c ; :: thesis: gg (*) c = gg
then A29: cod (id (cod f1)) = dom gg1 by CAT_1:def 6;
thus gg (*) c = gg1 (*) (id (cod f1)) by A28, A2
.= gg by A29, CAT_1:22 ; :: thesis: verum

end;

hence c is identity by A25, Def4, Def5; :: thesis: verum

end;

set d1 = id (dom f1);
A30: cod (id (dom f1)) = dom f1 ;
reconsider d = id (dom f1) as morphism of cc ;
take d ; :: thesis: ( f |> d & d is identity )
thus f |> d by A30, CAT_1:def 6; :: thesis: d is identity
A31: for ff being morphism of cc st d |> ff holds
d (*) ff = ff

proof

let ff be morphism of cc; :: thesis: ( d |> ff implies d (*) ff = ff )
reconsider ff1 = ff as Morphism of C ;
assume A32: d |> ff ; :: thesis: d (*) ff = ff
then A33: dom (id (dom f1)) = cod ff1 by CAT_1:def 6;
thus d (*) ff = (id (dom f1)) (*) ff1 by A32, A2
.= ff by A33, CAT_1:21 ; :: thesis: verum

end;

for gg being morphism of cc st gg |> d holds
gg (*) d = gg

proof

let gg be morphism of cc; :: thesis: ( gg |> d implies gg (*) d = gg )
reconsider gg1 = gg as Morphism of C ;
assume A34: gg |> d ; :: thesis: gg (*) d = gg
then A35: cod (id (dom f1)) = dom gg1 by CAT_1:def 6;
thus gg (*) d = gg1 (*) (id (dom f1)) by A34, A2
.= gg by A35, CAT_1:22 ; :: thesis: verum

end;

hence d is identity by A31, Def4, Def5; :: thesis: verum

end;

set CS = CategoryStr(# the carrier' of C, the Comp of C #);
CategoryStr(# the carrier' of C, the Comp of C #) is composable by A5, Lm3;
hence CategoryStr(# the carrier' of C, the Comp of C #) is category by A23, A16, Lm5, Lm2; :: thesis: verum