let C be Category; :: thesis: for O being non empty Subset of the carrier of C

for M being non empty set

for d, c being Function of M,O

for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

let O be non empty Subset of the carrier of C; :: thesis: for M being non empty set

for d, c being Function of M,O

for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

let M be non empty set ; :: thesis: for d, c being Function of M,O

for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

let d, c be Function of M,O; :: thesis: for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

let p be PartFunc of [:M,M:],M; :: thesis: for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

let i be Function of O,M; :: thesis: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is Category )

set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

assume that

A1: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } and

A2: d = the Source of C | M and

A3: c = the Target of C | M and

A4: p = the Comp of C || M ; :: thesis: CatStr(# O,M,d,c,p #) is Category

set B = CatStr(# O,M,d,c,p #);

( [g,f] in dom p iff d . g = c . f )

A11: CatStr(# O,M,d,c,p #) is transitive

for M being non empty set

for d, c being Function of M,O

for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

let O be non empty Subset of the carrier of C; :: thesis: for M being non empty set

for d, c being Function of M,O

for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

let M be non empty set ; :: thesis: for d, c being Function of M,O

for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

let d, c be Function of M,O; :: thesis: for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

let p be PartFunc of [:M,M:],M; :: thesis: for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

let i be Function of O,M; :: thesis: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is Category )

set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

assume that

A1: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } and

A2: d = the Source of C | M and

A3: c = the Target of C | M and

A4: p = the Comp of C || M ; :: thesis: CatStr(# O,M,d,c,p #) is Category

set B = CatStr(# O,M,d,c,p #);

A5: now :: thesis: for f being Morphism of CatStr(# O,M,d,c,p #) holds f is Morphism of C

A8:
for f, g being Morphism of CatStr(# O,M,d,c,p #) holds let f be Morphism of CatStr(# O,M,d,c,p #); :: thesis: f is Morphism of C

consider X being set such that

A6: f in X and

A7: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A1, TARSKI:def 4;

ex a, b being Object of C st

( X = Hom (a,b) & a in O & b in O ) by A7;

hence f is Morphism of C by A6; :: thesis: verum

end;consider X being set such that

A6: f in X and

A7: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A1, TARSKI:def 4;

ex a, b being Object of C st

( X = Hom (a,b) & a in O & b in O ) by A7;

hence f is Morphism of C by A6; :: thesis: verum

( [g,f] in dom p iff d . g = c . f )

proof

A10:
CatStr(# O,M,d,c,p #) is Category-like
by A8;
let f, g be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( [g,f] in dom p iff d . g = c . f )

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

A9: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;

thus ( [g,f] in dom p implies d . g = c . f ) :: thesis: ( d . g = c . f implies [g,f] in dom p )

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

then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def 4;

hence [g,f] in dom p by A4, RELAT_1:61; :: thesis: verum

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

A9: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;

thus ( [g,f] in dom p implies d . g = c . f ) :: thesis: ( d . g = c . f implies [g,f] in dom p )

proof

assume
d . g = c . f
; :: thesis: [g,f] in dom p
assume
[g,f] in dom p
; :: thesis: d . g = c . f

then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4, RELAT_1:61;

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

hence d . g = c . f by A9, CAT_1:def 6; :: thesis: verum

end;then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4, RELAT_1:61;

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

hence d . g = c . f by A9, CAT_1:def 6; :: thesis: verum

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

then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def 4;

hence [g,f] in dom p by A4, RELAT_1:61; :: thesis: verum

A11: CatStr(# O,M,d,c,p #) is transitive

proof

A18:
CatStr(# O,M,d,c,p #) is associative
thus
for f, g being Morphism of CatStr(# O,M,d,c,p #) st dom g = cod f holds

( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) :: according to CAT_1:def 7 :: thesis: verum

end;( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) :: according to CAT_1:def 7 :: thesis: verum

proof

let f, g be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )

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

A12: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;

assume A13: dom g = cod f ; :: thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )

A14: [g,f] in dom the Comp of CatStr(# O,M,d,c,p #) by A13, A8;

A15: p . (g,f) = g (*) f by A13, A8, CAT_1:def 1;

A16: dom p c= dom the Comp of C by A4, RELAT_1:60;

A17: p . [g,f] = the Comp of C . (g,f) by A4, A8, A13, FUNCT_1:47

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

thus dom (g (*) f) = dom (gg (*) ff) by A17, A2, A15, FUNCT_1:49

.= dom ff by A13, A12, CAT_1:def 7

.= dom f by A2, FUNCT_1:49 ; :: thesis: cod (g (*) f) = cod g

thus cod (g (*) f) = cod (gg (*) ff) by A17, A3, A15, FUNCT_1:49

.= cod gg by A13, A12, CAT_1:def 7

.= cod g by A3, FUNCT_1:49 ; :: thesis: verum

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

A12: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;

assume A13: dom g = cod f ; :: thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )

A14: [g,f] in dom the Comp of CatStr(# O,M,d,c,p #) by A13, A8;

A15: p . (g,f) = g (*) f by A13, A8, CAT_1:def 1;

A16: dom p c= dom the Comp of C by A4, RELAT_1:60;

A17: p . [g,f] = the Comp of C . (g,f) by A4, A8, A13, FUNCT_1:47

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

thus dom (g (*) f) = dom (gg (*) ff) by A17, A2, A15, FUNCT_1:49

.= dom ff by A13, A12, CAT_1:def 7

.= dom f by A2, FUNCT_1:49 ; :: thesis: cod (g (*) f) = cod g

thus cod (g (*) f) = cod (gg (*) ff) by A17, A3, A15, FUNCT_1:49

.= cod gg by A13, A12, CAT_1:def 7

.= cod g by A3, FUNCT_1:49 ; :: thesis: verum

proof

A34:
CatStr(# O,M,d,c,p #) is reflexive
thus
for f, g, h being Morphism of CatStr(# O,M,d,c,p #) st dom h = cod g & dom g = cod f holds

h (*) (g (*) f) = (h (*) g) (*) f :: according to CAT_1:def 8 :: thesis: verum

end;h (*) (g (*) f) = (h (*) g) (*) f :: according to CAT_1:def 8 :: thesis: verum

proof

let f, g, h be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )

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

assume that

A19: dom h = cod g and

A20: dom g = cod f ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f

A21: h (*) g = the Comp of CatStr(# O,M,d,c,p #) . (h,g) by A19, A8, CAT_1:def 1;

A22: g (*) f = the Comp of CatStr(# O,M,d,c,p #) . (g,f) by A20, A8, CAT_1:def 1;

A23: dom (h (*) g) = dom g by A11, A19;

A24: ( c . g = cod gg & d . g = dom gg ) by A2, A3, FUNCT_1:49;

A25: c . f = cod ff by A3, FUNCT_1:49;

A26: ( f is Morphism of C & d . h = dom hh ) by A2, A5, FUNCT_1:49;

A27: dom gg = d . g by A2, FUNCT_1:49

.= cod ff by A3, A20, FUNCT_1:49 ;

then A28: gg (*) ff = the Comp of C . (gg,ff) by CAT_1:16;

A29: dom hh = d . h by A2, FUNCT_1:49

.= cod gg by A3, A19, FUNCT_1:49 ;

then A30: cod (gg (*) ff) = dom hh by A27, CAT_1:def 7;

A31: hh (*) gg = the Comp of C . (hh,gg) by A29, CAT_1:16;

A32: cod ff = dom (hh (*) gg) by A27, A29, CAT_1:def 7;

A33: cod (g (*) f) = cod g by A11, A20;

hence h (*) (g (*) f) = the Comp of CatStr(# O,M,d,c,p #) . (h,( the Comp of CatStr(# O,M,d,c,p #) . (g,f))) by A22, A19, A8, CAT_1:def 1

.= the Comp of C . [h,(p . [g,f])] by A4, A8, A19, A33, A22, FUNCT_1:47

.= the Comp of C . (hh,(gg (*) ff)) by A4, A8, A20, A28, FUNCT_1:47

.= hh (*) (gg (*) ff) by A30, CAT_1:16

.= (hh (*) gg) (*) ff by A19, A20, A26, A24, A25, CAT_1:def 8

.= the Comp of C . (( the Comp of C . (hh,gg)),ff) by A31, A32, CAT_1:16

.= the Comp of C . [(p . [h,g]),f] by A4, A8, A19, FUNCT_1:47

.= the Comp of CatStr(# O,M,d,c,p #) . (( the Comp of CatStr(# O,M,d,c,p #) . (h,g)),f) by A4, A8, A20, A23, A21, FUNCT_1:47

.= (h (*) g) (*) f by A21, A20, A8, A23, CAT_1:def 1 ;

:: thesis: verum

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

assume that

A19: dom h = cod g and

A20: dom g = cod f ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f

A21: h (*) g = the Comp of CatStr(# O,M,d,c,p #) . (h,g) by A19, A8, CAT_1:def 1;

A22: g (*) f = the Comp of CatStr(# O,M,d,c,p #) . (g,f) by A20, A8, CAT_1:def 1;

A23: dom (h (*) g) = dom g by A11, A19;

A24: ( c . g = cod gg & d . g = dom gg ) by A2, A3, FUNCT_1:49;

A25: c . f = cod ff by A3, FUNCT_1:49;

A26: ( f is Morphism of C & d . h = dom hh ) by A2, A5, FUNCT_1:49;

A27: dom gg = d . g by A2, FUNCT_1:49

.= cod ff by A3, A20, FUNCT_1:49 ;

then A28: gg (*) ff = the Comp of C . (gg,ff) by CAT_1:16;

A29: dom hh = d . h by A2, FUNCT_1:49

.= cod gg by A3, A19, FUNCT_1:49 ;

then A30: cod (gg (*) ff) = dom hh by A27, CAT_1:def 7;

A31: hh (*) gg = the Comp of C . (hh,gg) by A29, CAT_1:16;

A32: cod ff = dom (hh (*) gg) by A27, A29, CAT_1:def 7;

A33: cod (g (*) f) = cod g by A11, A20;

hence h (*) (g (*) f) = the Comp of CatStr(# O,M,d,c,p #) . (h,( the Comp of CatStr(# O,M,d,c,p #) . (g,f))) by A22, A19, A8, CAT_1:def 1

.= the Comp of C . [h,(p . [g,f])] by A4, A8, A19, A33, A22, FUNCT_1:47

.= the Comp of C . (hh,(gg (*) ff)) by A4, A8, A20, A28, FUNCT_1:47

.= hh (*) (gg (*) ff) by A30, CAT_1:16

.= (hh (*) gg) (*) ff by A19, A20, A26, A24, A25, CAT_1:def 8

.= the Comp of C . (( the Comp of C . (hh,gg)),ff) by A31, A32, CAT_1:16

.= the Comp of C . [(p . [h,g]),f] by A4, A8, A19, FUNCT_1:47

.= the Comp of CatStr(# O,M,d,c,p #) . (( the Comp of CatStr(# O,M,d,c,p #) . (h,g)),f) by A4, A8, A20, A23, A21, FUNCT_1:47

.= (h (*) g) (*) f by A21, A20, A8, A23, CAT_1:def 1 ;

:: thesis: verum

proof

CatStr(# O,M,d,c,p #) is with_identities
let b be Object of CatStr(# O,M,d,c,p #); :: according to CAT_1:def 9 :: thesis: not Hom (b,b) = {}

b in O ;

then reconsider bb = b as Object of C ;

A35: Hom (bb,bb) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

id bb in Hom (bb,bb) by CAT_1:27;

then reconsider ii = id bb as Morphism of CatStr(# O,M,d,c,p #) by A35, A1, TARSKI:def 4;

A36: dom ii = dom (id bb) by A2, FUNCT_1:49

.= bb ;

cod ii = cod (id bb) by A3, FUNCT_1:49

.= bb ;

then ii in Hom (b,b) by A36;

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

end;b in O ;

then reconsider bb = b as Object of C ;

A35: Hom (bb,bb) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

id bb in Hom (bb,bb) by CAT_1:27;

then reconsider ii = id bb as Morphism of CatStr(# O,M,d,c,p #) by A35, A1, TARSKI:def 4;

A36: dom ii = dom (id bb) by A2, FUNCT_1:49

.= bb ;

cod ii = cod (id bb) by A3, FUNCT_1:49

.= bb ;

then ii in Hom (b,b) by A36;

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

proof

hence
CatStr(# O,M,d,c,p #) is Category
by A10, A11, A18, A34; :: thesis: verum
let a be Element of CatStr(# O,M,d,c,p #); :: 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 CatStr(# O,M,d,c,p #) 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} ) )

a in O ;

then reconsider aa = a as Object of C ;

A37: Hom (aa,aa) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

id aa in Hom (aa,aa) by CAT_1:27;

then reconsider ii = id aa as Morphism of CatStr(# O,M,d,c,p #) by A37, A1, TARSKI:def 4;

A38: dom ii = dom (id aa) by A2, FUNCT_1:49

.= aa ;

A39: cod ii = cod (id aa) by A3, FUNCT_1:49

.= aa ;

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

take ii ; :: thesis: for b_{1} being Element of the carrier of CatStr(# O,M,d,c,p #) 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 CatStr(# O,M,d,c,p #); :: 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} ) )

b in O ;

then reconsider bb = b as Object 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} )

end;for b

( ( Hom (a,b

a in O ;

then reconsider aa = a as Object of C ;

A37: Hom (aa,aa) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

id aa in Hom (aa,aa) by CAT_1:27;

then reconsider ii = id aa as Morphism of CatStr(# O,M,d,c,p #) by A37, A1, TARSKI:def 4;

A38: dom ii = dom (id aa) by A2, FUNCT_1:49

.= aa ;

A39: cod ii = cod (id aa) by A3, FUNCT_1:49

.= aa ;

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

take ii ; :: thesis: for b

( ( Hom (a,b

let b be Element of CatStr(# O,M,d,c,p #); :: thesis: ( ( Hom (a,b) = {} or for b

b in O ;

then reconsider bb = b as Object 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

thus
( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )
:: thesis: verum
assume A40:
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 by A5;

A41: dom gg = dom g by A2, FUNCT_1:49

.= aa by A40, CAT_1:5 ;

A42: cod (id aa) = aa ;

cod gg = cod g by A3, FUNCT_1:49

.= bb by A40, CAT_1:5 ;

then reconsider gg = gg as Morphism of aa,bb by A41, CAT_1:4;

A43: dom g = a by A40, CAT_1:5;

hence g (*) ii = p . (g,ii) by A39, A8, CAT_1:def 1

.= the Comp of C . (gg,(id aa)) by A43, A4, A39, A8, FUNCT_1:47

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

.= g by A41, CAT_1:22 ;

:: thesis: verum

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

reconsider gg = g as Morphism of C by A5;

A41: dom gg = dom g by A2, FUNCT_1:49

.= aa by A40, CAT_1:5 ;

A42: cod (id aa) = aa ;

cod gg = cod g by A3, FUNCT_1:49

.= bb by A40, CAT_1:5 ;

then reconsider gg = gg as Morphism of aa,bb by A41, CAT_1:4;

A43: dom g = a by A40, CAT_1:5;

hence g (*) ii = p . (g,ii) by A39, A8, CAT_1:def 1

.= the Comp of C . (gg,(id aa)) by A43, A4, A39, A8, FUNCT_1:47

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

.= g by A41, CAT_1:22 ;

:: thesis: verum

proof

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

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

reconsider gg = g as Morphism of C by A5;

A45: cod gg = cod g by A3, FUNCT_1:49

.= aa by A44, CAT_1:5 ;

A46: dom (id aa) = aa ;

dom gg = dom g by A2, FUNCT_1:49

.= bb by A44, CAT_1:5 ;

then reconsider gg = gg as Morphism of bb,aa by A45, CAT_1:4;

A47: cod g = a by A44, CAT_1:5;

hence ii (*) g = p . (ii,g) by A38, A8, CAT_1:def 1

.= the Comp of C . ((id aa),gg) by A4, A47, A38, A8, FUNCT_1:47

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

.= g by A45, CAT_1:21 ;

:: thesis: verum

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

reconsider gg = g as Morphism of C by A5;

A45: cod gg = cod g by A3, FUNCT_1:49

.= aa by A44, CAT_1:5 ;

A46: dom (id aa) = aa ;

dom gg = dom g by A2, FUNCT_1:49

.= bb by A44, CAT_1:5 ;

then reconsider gg = gg as Morphism of bb,aa by A45, CAT_1:4;

A47: cod g = a by A44, CAT_1:5;

hence ii (*) g = p . (ii,g) by A38, A8, CAT_1:def 1

.= the Comp of C . ((id aa),gg) by A4, A47, A38, A8, FUNCT_1:47

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

.= g by A45, CAT_1:21 ;

:: thesis: verum