set M = Maps V;

set d = fDom V;

set c = fCod V;

set p = fComp V;

reconsider C = CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #) as non empty non void CatStr ;

A1: C is Category-like

set d = fDom V;

set c = fCod V;

set p = fComp V;

reconsider C = CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #) as non empty non void CatStr ;

A1: C is Category-like

proof

A2:
C is transitive
let ff, gg be Morphism of C; :: according to CAT_1:def 6 :: thesis: ( ( not [gg,ff] in proj1 the Comp of C or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of C ) )

reconsider f = ff, g = gg as Element of Maps V ;

( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def9, Def10;

hence ( ( not [gg,ff] in proj1 the Comp of C or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of C ) ) by Def11; :: thesis: verum

end;reconsider f = ff, g = gg as Element of Maps V ;

( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def9, Def10;

hence ( ( not [gg,ff] in proj1 the Comp of C or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in proj1 the Comp of C ) ) by Def11; :: thesis: verum

proof

A8:
C is associative
let ff, gg be Morphism of C; :: according to CAT_1:def 7 :: thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )

assume A3: dom gg = cod ff ; :: thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )

[gg,ff] in dom the Comp of C by A3, A1;

then A4: the Comp of C . (gg,ff) = gg (*) ff by CAT_1:def 1;

reconsider f = ff, g = gg as Element of Maps V ;

A5: ( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def9, Def10;

then A6: (fComp V) . [g,f] = g * f by A3, Def11;

A7: ( (fDom V) . f = dom f & (fCod V) . g = cod g ) by Def9, Def10;

( dom (g * f) = dom f & cod (g * f) = cod g ) by A3, A5, Th12;

hence ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) by A6, A7, Def9, Def10, A4; :: thesis: verum

end;assume A3: dom gg = cod ff ; :: thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )

[gg,ff] in dom the Comp of C by A3, A1;

then A4: the Comp of C . (gg,ff) = gg (*) ff by CAT_1:def 1;

reconsider f = ff, g = gg as Element of Maps V ;

A5: ( (fDom V) . g = dom g & (fCod V) . f = cod f ) by Def9, Def10;

then A6: (fComp V) . [g,f] = g * f by A3, Def11;

A7: ( (fDom V) . f = dom f & (fCod V) . g = cod g ) by Def9, Def10;

( dom (g * f) = dom f & cod (g * f) = cod g ) by A3, A5, Th12;

hence ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) by A6, A7, Def9, Def10, A4; :: thesis: verum

proof

A18:
C is reflexive
let ff, gg, hh be Morphism of C; :: according to CAT_1:def 8 :: thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff )

assume that

A9: dom hh = cod gg and

A10: dom gg = cod ff ; :: thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff

reconsider f = ff, g = gg, h = hh as Element of Maps V ;

A11: ( dom h = (fDom V) . h & cod g = (fCod V) . g ) by Def9, Def10;

then A12: dom (h * g) = dom g by A9, Th12;

A13: ( dom g = (fDom V) . g & cod f = (fCod V) . f ) by Def9, Def10;

then A14: cod (g * f) = dom h by A9, A10, A11, Th12;

[hh,gg] in dom the Comp of C by A9, A1;

then A15: hh (*) gg = the Comp of C . (hh,gg) by CAT_1:def 1;

dom (hh (*) gg) = dom gg by A2, A9;

then A16: [(hh (*) gg),ff] in dom the Comp of C by A1, A10;

[gg,ff] in dom the Comp of C by A10, A1;

then A17: gg (*) ff = the Comp of C . (gg,ff) by CAT_1:def 1;

cod (gg (*) ff) = cod gg by A2, A10;

then [hh,(gg (*) ff)] in dom the Comp of C by A1, A9;

hence hh (*) (gg (*) ff) = the Comp of C . (hh,( the Comp of C . (gg,ff))) by A17, CAT_1:def 1

.= (fComp V) . [h,(g * f)] by A10, A13, Def11

.= h * (g * f) by A14, Def11

.= (h * g) * f by A9, A10, A11, A13, Th13

.= (fComp V) . [(h * g),f] by A10, A13, A12, Def11

.= the Comp of C . (( the Comp of C . (hh,gg)),ff) by A9, A11, Def11

.= (hh (*) gg) (*) ff by A16, A15, CAT_1:def 1 ;

:: thesis: verum

end;assume that

A9: dom hh = cod gg and

A10: dom gg = cod ff ; :: thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff

reconsider f = ff, g = gg, h = hh as Element of Maps V ;

A11: ( dom h = (fDom V) . h & cod g = (fCod V) . g ) by Def9, Def10;

then A12: dom (h * g) = dom g by A9, Th12;

A13: ( dom g = (fDom V) . g & cod f = (fCod V) . f ) by Def9, Def10;

then A14: cod (g * f) = dom h by A9, A10, A11, Th12;

[hh,gg] in dom the Comp of C by A9, A1;

then A15: hh (*) gg = the Comp of C . (hh,gg) by CAT_1:def 1;

dom (hh (*) gg) = dom gg by A2, A9;

then A16: [(hh (*) gg),ff] in dom the Comp of C by A1, A10;

[gg,ff] in dom the Comp of C by A10, A1;

then A17: gg (*) ff = the Comp of C . (gg,ff) by CAT_1:def 1;

cod (gg (*) ff) = cod gg by A2, A10;

then [hh,(gg (*) ff)] in dom the Comp of C by A1, A9;

hence hh (*) (gg (*) ff) = the Comp of C . (hh,( the Comp of C . (gg,ff))) by A17, CAT_1:def 1

.= (fComp V) . [h,(g * f)] by A10, A13, Def11

.= h * (g * f) by A14, Def11

.= (h * g) * f by A9, A10, A11, A13, Th13

.= (fComp V) . [(h * g),f] by A10, A13, A12, Def11

.= the Comp of C . (( the Comp of C . (hh,gg)),ff) by A9, A11, Def11

.= (hh (*) gg) (*) ff by A16, A15, CAT_1:def 1 ;

:: thesis: verum

proof

C is with_identities
let a be Element of C; :: according to CAT_1:def 9 :: thesis: not Hom (a,a) = {}

reconsider aa = a as Element of V ;

reconsider ii = id$ aa as Morphism of C ;

A19: cod ii = cod (id$ aa) by Def10

.= a ;

dom ii = dom (id$ aa) by Def9

.= a ;

then ii in Hom (a,a) by A19;

hence Hom (a,a) <> {} ; :: thesis: verum

end;reconsider aa = a as Element of V ;

reconsider ii = id$ aa as Morphism of C ;

A19: cod ii = cod (id$ aa) by Def10

.= a ;

dom ii = dom (id$ aa) by Def9

.= a ;

then ii in Hom (a,a) by A19;

hence Hom (a,a) <> {} ; :: thesis: verum

proof

hence
( Ens V is Category-like & Ens V is reflexive & Ens V is transitive & Ens V is associative & Ens V is with_identities )
by A1, A2, A8, A18; :: thesis: verum
let a be Element of C; :: according to CAT_1:def 10 :: thesis: ex b_{1} being Morphism of a,a st

for b_{2} being Element of the carrier of C holds

( ( Hom (a,b_{2}) = {} or for b_{3} being Morphism of a,b_{2} holds b_{3} (*) b_{1} = b_{3} ) & ( Hom (b_{2},a) = {} or for b_{3} being Morphism of b_{2},a holds b_{1} (*) b_{3} = b_{3} ) )

reconsider aa = a as Element of V ;

reconsider ii = id$ aa as Morphism of C ;

A20: cod ii = cod (id$ aa) by Def10

.= a ;

A21: dom ii = dom (id$ aa) by Def9

.= a ;

then reconsider ii = ii as Morphism of a,a by A20, CAT_1:4;

take ii ; :: thesis: for b_{1} being Element of the carrier of C holds

( ( Hom (a,b_{1}) = {} or for b_{2} being Morphism of a,b_{1} holds b_{2} (*) ii = b_{2} ) & ( Hom (b_{1},a) = {} or for b_{2} being Morphism of b_{1},a holds ii (*) b_{2} = b_{2} ) )

let b be Element of C; :: thesis: ( ( Hom (a,b) = {} or for b_{1} being Morphism of a,b holds b_{1} (*) ii = b_{1} ) & ( Hom (b,a) = {} or for b_{1} being Morphism of b,a holds ii (*) b_{1} = b_{1} ) )

thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) :: thesis: ( Hom (b,a) = {} or for b_{1} being Morphism of b,a holds ii (*) b_{1} = b_{1} )_{1} being Morphism of b,a holds ii (*) b_{1} = b_{1}

let g be Morphism of b,a; :: thesis: ii (*) g = g

reconsider gg = g as Element of Maps V ;

A26: cod gg = cod g by Def10

.= aa by A25, CAT_1:5 ;

then A27: dom (id$ aa) = cod gg ;

cod g = a by A25, CAT_1:5;

then [ii,g] in dom (fComp V) by A21, A1;

hence ii (*) g = (fComp V) . (ii,g) by CAT_1:def 1

.= (id$ aa) * gg by A27, Def11

.= g by A26, Th14 ;

:: thesis: verum

end;for b

( ( Hom (a,b

reconsider aa = a as Element of V ;

reconsider ii = id$ aa as Morphism of C ;

A20: cod ii = cod (id$ aa) by Def10

.= a ;

A21: dom ii = dom (id$ aa) by Def9

.= a ;

then reconsider ii = ii as Morphism of a,a by A20, CAT_1:4;

take ii ; :: thesis: for b

( ( Hom (a,b

let b be Element of C; :: thesis: ( ( Hom (a,b) = {} or for b

thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) :: thesis: ( Hom (b,a) = {} or for b

proof

assume A25:
Hom (b,a) <> {}
; :: thesis: for b
assume A22:
Hom (a,b) <> {}
; :: thesis: for g being Morphism of a,b holds g (*) ii = g

let g be Morphism of a,b; :: thesis: g (*) ii = g

reconsider gg = g as Element of Maps V ;

A23: dom gg = dom g by Def9

.= aa by A22, CAT_1:5 ;

then A24: cod (id$ aa) = dom gg ;

dom g = a by A22, CAT_1:5;

then [g,ii] in dom (fComp V) by A20, A1;

hence g (*) ii = (fComp V) . (g,ii) by CAT_1:def 1

.= gg * (id$ aa) by A24, Def11

.= g by A23, Th14 ;

:: thesis: verum

end;let g be Morphism of a,b; :: thesis: g (*) ii = g

reconsider gg = g as Element of Maps V ;

A23: dom gg = dom g by Def9

.= aa by A22, CAT_1:5 ;

then A24: cod (id$ aa) = dom gg ;

dom g = a by A22, CAT_1:5;

then [g,ii] in dom (fComp V) by A20, A1;

hence g (*) ii = (fComp V) . (g,ii) by CAT_1:def 1

.= gg * (id$ aa) by A24, Def11

.= g by A23, Th14 ;

:: thesis: verum

let g be Morphism of b,a; :: thesis: ii (*) g = g

reconsider gg = g as Element of Maps V ;

A26: cod gg = cod g by Def10

.= aa by A25, CAT_1:5 ;

then A27: dom (id$ aa) = cod gg ;

cod g = a by A25, CAT_1:5;

then [ii,g] in dom (fComp V) by A21, A1;

hence ii (*) g = (fComp V) . (ii,g) by CAT_1:def 1

.= (id$ aa) * gg by A27, Def11

.= g by A26, Th14 ;

:: thesis: verum