set M = the carrier' of C;

set d = the Target of C;

set c = the Source of C;

set p = ~ the Comp of C;

set B = C opp ;

thus A1: C opp is Category-like :: thesis: ( C opp is transitive & C opp is associative & C opp is reflexive & C opp is with_identities )

(~ the Comp of C) . (g,f) = the Comp of C . (f,g)_{1} being Morphism of a,a st

for b_{2} being Element of the carrier of (C opp) 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 C ;

reconsider ii = id aa as Morphism of (C opp) ;

A29: dom ii = cod (id aa)

.= aa ;

A30: cod ii = dom (id aa)

.= aa ;

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

take ii ; :: thesis: for b_{1} being Element of the carrier of (C opp) 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 opp); :: 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} ) )

reconsider bb = b as Element of C ;

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 Morphism of C ;

A37: cod gg = dom g

.= bb by A36, CAT_1:5 ;

A38: dom gg = cod g

.= aa by A36, CAT_1:5 ;

then A39: dom gg = cod (id aa) ;

reconsider gg = gg as Morphism of aa,bb by A37, A38, CAT_1:4;

A40: the Target of C . ii = aa by A29

.= cod g by A36, CAT_1:5

.= the Source of C . g ;

then cod g = dom ii ;

then [ii,g] in dom the Comp of (C opp) by A1;

hence ii (*) g = (~ the Comp of C) . (ii,g) by CAT_1:def 1

.= the Comp of C . (g,ii) by A40, A3

.= gg (*) (id aa) by A39, CAT_1:16

.= g by A38, CAT_1:22 ;

:: thesis: verum

set d = the Target of C;

set c = the Source of C;

set p = ~ the Comp of C;

set B = C opp ;

thus A1: C opp is Category-like :: thesis: ( C opp is transitive & C opp is associative & C opp is reflexive & C opp is with_identities )

proof

A3:
for f, g being Element of the carrier' of C st the Target of C . g = the Source of C . f holds
let f, g be Morphism of (C opp); :: according to CAT_1:def 6 :: thesis: ( ( not [g,f] in dom the Comp of (C opp) or dom g = cod f ) & ( not dom g = cod f or [g,f] in dom the Comp of (C opp) ) )

reconsider ff = f, gg = g as Morphism of C ;

thus ( [g,f] in dom the Comp of (C opp) implies dom g = cod f ) :: thesis: ( not dom g = cod f or [g,f] in dom the Comp of (C opp) )

cod gg = dom ff by A2;

then [ff,gg] in dom the Comp of C by CAT_1:def 6;

hence [g,f] in dom the Comp of (C opp) by FUNCT_4:42; :: thesis: verum

end;reconsider ff = f, gg = g as Morphism of C ;

thus ( [g,f] in dom the Comp of (C opp) implies dom g = cod f ) :: thesis: ( not dom g = cod f or [g,f] in dom the Comp of (C opp) )

proof

assume A2:
dom g = cod f
; :: thesis: [g,f] in dom the Comp of (C opp)
assume
[g,f] in dom the Comp of (C opp)
; :: thesis: dom g = cod f

then [ff,gg] in dom the Comp of C by FUNCT_4:42;

then dom ff = cod gg by CAT_1:def 6;

hence dom g = cod f ; :: thesis: verum

end;then [ff,gg] in dom the Comp of C by FUNCT_4:42;

then dom ff = cod gg by CAT_1:def 6;

hence dom g = cod f ; :: thesis: verum

cod gg = dom ff by A2;

then [ff,gg] in dom the Comp of C by CAT_1:def 6;

hence [g,f] in dom the Comp of (C opp) by FUNCT_4:42; :: thesis: verum

(~ the Comp of C) . (g,f) = the Comp of C . (f,g)

proof

thus A4:
C opp is transitive
:: thesis: ( C opp is associative & C opp is reflexive & C opp is with_identities )
let f, g be Element of the carrier' of C; :: thesis: ( the Target of C . g = the Source of C . f implies (~ the Comp of C) . (g,f) = the Comp of C . (f,g) )

reconsider ff = f, gg = g as Morphism of (C opp) ;

assume the Target of C . g = the Source of C . f ; :: thesis: (~ the Comp of C) . (g,f) = the Comp of C . (f,g)

then dom gg = cod ff ;

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

hence (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by FUNCT_4:43; :: thesis: verum

end;reconsider ff = f, gg = g as Morphism of (C opp) ;

assume the Target of C . g = the Source of C . f ; :: thesis: (~ the Comp of C) . (g,f) = the Comp of C . (f,g)

then dom gg = cod ff ;

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

hence (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by FUNCT_4:43; :: thesis: verum

proof

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

reconsider f = ff, g = gg as Morphism of C ;

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

then A6: cod g = dom f ;

then A7: [f,g] in dom the Comp of C by CAT_1:def 6;

[gg,ff] in dom the Comp of (C opp) by A5, A1;

then A8: gg (*) ff = (~ the Comp of C) . (g,f) by CAT_1:def 1

.= the Comp of C . (f,g) by A3, A5

.= f (*) g by A7, CAT_1:def 1 ;

hence dom (gg (*) ff) = cod (f (*) g)

.= cod f by A6, CAT_1:def 7

.= dom ff ;

:: thesis: cod (gg (*) ff) = cod gg

thus cod (gg (*) ff) = dom (f (*) g) by A8

.= dom g by A6, CAT_1:def 7

.= cod gg ; :: thesis: verum

end;reconsider f = ff, g = gg as Morphism of C ;

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

then A6: cod g = dom f ;

then A7: [f,g] in dom the Comp of C by CAT_1:def 6;

[gg,ff] in dom the Comp of (C opp) by A5, A1;

then A8: gg (*) ff = (~ the Comp of C) . (g,f) by CAT_1:def 1

.= the Comp of C . (f,g) by A3, A5

.= f (*) g by A7, CAT_1:def 1 ;

hence dom (gg (*) ff) = cod (f (*) g)

.= cod f by A6, CAT_1:def 7

.= dom ff ;

:: thesis: cod (gg (*) ff) = cod gg

thus cod (gg (*) ff) = dom (f (*) g) by A8

.= dom g by A6, CAT_1:def 7

.= cod gg ; :: thesis: verum

proof

thus
C opp is reflexive
:: thesis: C opp is with_identities
let ff, gg, hh be Morphism of (C opp); :: 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 )

reconsider f = ff, g = gg, h = hh as Morphism of C ;

assume that

A9: dom hh = cod gg and

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

A11: [h,g] in dom (~ the Comp of C) by A1, A9;

then A12: (~ the Comp of C) . (h,g) is Element of the carrier' of C by PARTFUN1:4;

A13: [g,f] in dom (~ the Comp of C) by A1, A10;

then A14: (~ the Comp of C) . (g,f) is Element of the carrier' of C by PARTFUN1:4;

A15: (~ the Comp of C) . (h,g) = the Comp of C . (g,h) by A3, A9;

the Target of C . ((~ the Comp of C) . (h,g)) = dom (hh (*) gg) by A11, CAT_1:def 1

.= dom gg by A4, A9 ;

then A16: (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) = the Comp of C . (f,( the Comp of C . (g,h))) by A3, A10, A12, A15;

A17: ( cod h = dom g & cod g = dom f ) by A9, A10;

A18: (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by A3, A10;

A19: the Source of C . ((~ the Comp of C) . (g,f)) = cod (gg (*) ff) by A13, CAT_1:def 1

.= cod gg by A4, A10 ;

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

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

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

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

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

then A22: hh (*) gg = (~ the Comp of C) . (h,g) by CAT_1:def 1;

A23: f (*) g = the Comp of C . (f,g) by A17, CAT_1:16;

A24: dom (f (*) g) = dom g by A17, CAT_1:def 7;

A25: g (*) h = the Comp of C . (g,h) by A17, CAT_1:16;

A26: cod (g (*) h) = cod g by A17, CAT_1:def 7;

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

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

hence hh (*) (gg (*) ff) = (~ the Comp of C) . (h,((~ the Comp of C) . (g,f))) by A21, CAT_1:def 1

.= the Comp of C . (( the Comp of C . (f,g)),h) by A3, A9, A14, A18, A19

.= (f (*) g) (*) h by A23, A17, A24, CAT_1:16

.= f (*) (g (*) h) by A17, CAT_1:def 8

.= (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) by A16, A17, A25, A26, CAT_1:16

.= (hh (*) gg) (*) ff by A20, A22, CAT_1:def 1 ;

:: thesis: verum

end;reconsider f = ff, g = gg, h = hh as Morphism of C ;

assume that

A9: dom hh = cod gg and

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

A11: [h,g] in dom (~ the Comp of C) by A1, A9;

then A12: (~ the Comp of C) . (h,g) is Element of the carrier' of C by PARTFUN1:4;

A13: [g,f] in dom (~ the Comp of C) by A1, A10;

then A14: (~ the Comp of C) . (g,f) is Element of the carrier' of C by PARTFUN1:4;

A15: (~ the Comp of C) . (h,g) = the Comp of C . (g,h) by A3, A9;

the Target of C . ((~ the Comp of C) . (h,g)) = dom (hh (*) gg) by A11, CAT_1:def 1

.= dom gg by A4, A9 ;

then A16: (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) = the Comp of C . (f,( the Comp of C . (g,h))) by A3, A10, A12, A15;

A17: ( cod h = dom g & cod g = dom f ) by A9, A10;

A18: (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by A3, A10;

A19: the Source of C . ((~ the Comp of C) . (g,f)) = cod (gg (*) ff) by A13, CAT_1:def 1

.= cod gg by A4, A10 ;

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

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

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

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

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

then A22: hh (*) gg = (~ the Comp of C) . (h,g) by CAT_1:def 1;

A23: f (*) g = the Comp of C . (f,g) by A17, CAT_1:16;

A24: dom (f (*) g) = dom g by A17, CAT_1:def 7;

A25: g (*) h = the Comp of C . (g,h) by A17, CAT_1:16;

A26: cod (g (*) h) = cod g by A17, CAT_1:def 7;

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

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

hence hh (*) (gg (*) ff) = (~ the Comp of C) . (h,((~ the Comp of C) . (g,f))) by A21, CAT_1:def 1

.= the Comp of C . (( the Comp of C . (f,g)),h) by A3, A9, A14, A18, A19

.= (f (*) g) (*) h by A23, A17, A24, CAT_1:16

.= f (*) (g (*) h) by A17, CAT_1:def 8

.= (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) by A16, A17, A25, A26, CAT_1:16

.= (hh (*) gg) (*) ff by A20, A22, CAT_1:def 1 ;

:: thesis: verum

proof

let a be Element of (C opp); :: according to CAT_1:def 10 :: thesis: ex b
let bb be Object of (C opp); :: according to CAT_1:def 9 :: thesis: not Hom (bb,bb) = {}

reconsider b = bb as Element of C ;

consider f being Morphism of C such that

A27: f in Hom (b,b) by SUBSET_1:4;

reconsider ff = f as Morphism of (C opp) ;

A28: dom ff = cod f

.= bb by A27, CAT_1:1 ;

cod ff = dom f

.= bb by A27, CAT_1:1 ;

then ff in Hom (bb,bb) by A28;

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

end;reconsider b = bb as Element of C ;

consider f being Morphism of C such that

A27: f in Hom (b,b) by SUBSET_1:4;

reconsider ff = f as Morphism of (C opp) ;

A28: dom ff = cod f

.= bb by A27, CAT_1:1 ;

cod ff = dom f

.= bb by A27, CAT_1:1 ;

then ff in Hom (bb,bb) by A28;

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

for b

( ( Hom (a,b

reconsider aa = a as Element of C ;

reconsider ii = id aa as Morphism of (C opp) ;

A29: dom ii = cod (id aa)

.= aa ;

A30: cod ii = dom (id aa)

.= aa ;

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

take ii ; :: thesis: for b

( ( Hom (a,b

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

reconsider bb = b as Element of C ;

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 A36:
Hom (b,a) <> {}
; :: thesis: for b
assume A31:
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 Morphism of C ;

A32: dom gg = cod g

.= bb by A31, CAT_1:5 ;

A33: cod gg = dom g

.= aa by A31, CAT_1:5 ;

then A34: cod gg = dom (id aa) ;

reconsider gg = gg as Morphism of bb,aa by A32, A33, CAT_1:4;

A35: the Source of C . ii = aa by A30

.= dom g by A31, CAT_1:5

.= the Target of C . g ;

then dom g = cod ii ;

then [g,ii] in dom the Comp of (C opp) by A1;

hence g (*) ii = (~ the Comp of C) . (g,ii) by CAT_1:def 1

.= the Comp of C . (ii,g) by A35, A3

.= (id aa) (*) gg by A34, CAT_1:16

.= g by A33, CAT_1:21 ;

:: thesis: verum

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

reconsider gg = g as Morphism of C ;

A32: dom gg = cod g

.= bb by A31, CAT_1:5 ;

A33: cod gg = dom g

.= aa by A31, CAT_1:5 ;

then A34: cod gg = dom (id aa) ;

reconsider gg = gg as Morphism of bb,aa by A32, A33, CAT_1:4;

A35: the Source of C . ii = aa by A30

.= dom g by A31, CAT_1:5

.= the Target of C . g ;

then dom g = cod ii ;

then [g,ii] in dom the Comp of (C opp) by A1;

hence g (*) ii = (~ the Comp of C) . (g,ii) by CAT_1:def 1

.= the Comp of C . (ii,g) by A35, A3

.= (id aa) (*) gg by A34, CAT_1:16

.= g by A33, CAT_1:21 ;

:: thesis: verum

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

reconsider gg = g as Morphism of C ;

A37: cod gg = dom g

.= bb by A36, CAT_1:5 ;

A38: dom gg = cod g

.= aa by A36, CAT_1:5 ;

then A39: dom gg = cod (id aa) ;

reconsider gg = gg as Morphism of aa,bb by A37, A38, CAT_1:4;

A40: the Target of C . ii = aa by A29

.= cod g by A36, CAT_1:5

.= the Source of C . g ;

then cod g = dom ii ;

then [ii,g] in dom the Comp of (C opp) by A1;

hence ii (*) g = (~ the Comp of C) . (ii,g) by CAT_1:def 1

.= the Comp of C . (g,ii) by A40, A3

.= gg (*) (id aa) by A39, CAT_1:16

.= g by A38, CAT_1:22 ;

:: thesis: verum