set O = [: the carrier of C, the carrier of D:];

set M = [: the carrier' of C, the carrier' of D:];

set d = [: the Source of C, the Source of D:];

set c = [: the Target of C, the Target of D:];

set p = |: the Comp of C, the Comp of D:|;

A1: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds

( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D )

( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) )

A6: CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category-like

( [g,f] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) iff dom g = cod f ) by A6;

A11: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds

|: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))]

( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g )

set M = [: the carrier' of C, the carrier' of D:];

set d = [: the Source of C, the Source of D:];

set c = [: the Target of C, the Target of D:];

set p = |: the Comp of C, the Comp of D:|;

A1: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds

( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D )

proof

A4:
for f, g being Element of [: the carrier' of C, the carrier' of D:] st [g,f] in dom |: the Comp of C, the Comp of D:| holds
let f, g be Element of [: the carrier' of C, the carrier' of D:]; :: thesis: ( [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f implies ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) )

A2: ( [: the Source of C, the Source of D:] . ((g `1),(g `2)) = [( the Source of C . (g `1)),( the Source of D . (g `2))] & [: the Target of C, the Target of D:] . ((f `1),(f `2)) = [( the Target of C . (f `1)),( the Target of D . (f `2))] ) by FUNCT_3:75;

assume A3: [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; :: thesis: ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D )

( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;

then ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) by A2, A3, XTUPLE_0:1;

hence ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by CAT_1:def 6; :: thesis: verum

end;A2: ( [: the Source of C, the Source of D:] . ((g `1),(g `2)) = [( the Source of C . (g `1)),( the Source of D . (g `2))] & [: the Target of C, the Target of D:] . ((f `1),(f `2)) = [( the Target of C . (f `1)),( the Target of D . (f `2))] ) by FUNCT_3:75;

assume A3: [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; :: thesis: ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D )

( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;

then ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) by A2, A3, XTUPLE_0:1;

hence ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by CAT_1:def 6; :: thesis: verum

( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) )

proof

set B = CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #);
let f, g be Element of [: the carrier' of C, the carrier' of D:]; :: thesis: ( [g,f] in dom |: the Comp of C, the Comp of D:| implies ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) )

assume A5: [g,f] in dom |: the Comp of C, the Comp of D:| ; :: thesis: ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) )

( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;

then ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by A5, FUNCT_4:54;

hence ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) by CAT_1:def 6; :: thesis: verum

end;assume A5: [g,f] in dom |: the Comp of C, the Comp of D:| ; :: thesis: ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) )

( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;

then ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by A5, FUNCT_4:54;

hence ( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) ) by CAT_1:def 6; :: thesis: verum

A6: CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category-like

proof

A10:
for f, g being Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) holds
let ff, gg be Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def 6 :: thesis: ( ( not [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) or dom gg = cod ff ) & ( not dom gg = cod ff or [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ) )

reconsider f = ff, g = gg as Element of [: the carrier' of C, the carrier' of D:] ;

A7: ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;

thus ( [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) implies dom gg = cod ff ) :: thesis: ( not dom gg = cod ff or [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) )

then ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by A1;

hence [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A7, FUNCT_4:54; :: thesis: verum

end;reconsider f = ff, g = gg as Element of [: the carrier' of C, the carrier' of D:] ;

A7: ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;

thus ( [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) implies dom gg = cod ff ) :: thesis: ( not dom gg = cod ff or [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) )

proof

assume
dom gg = cod ff
; :: thesis: [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #)
A8:
( [: the Source of C, the Source of D:] . ((g `1),(g `2)) = [(dom (g `1)),(dom (g `2))] & [: the Target of C, the Target of D:] . ((f `1),(f `2)) = [(cod (f `1)),(cod (f `2))] )
by FUNCT_3:75;

assume A9: [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ; :: thesis: dom gg = cod ff

then dom (g `1) = cod (f `1) by A4;

hence dom gg = cod ff by A4, A7, A9, A8; :: thesis: verum

end;assume A9: [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ; :: thesis: dom gg = cod ff

then dom (g `1) = cod (f `1) by A4;

hence dom gg = cod ff by A4, A7, A9, A8; :: thesis: verum

then ( [(g `1),(f `1)] in dom the Comp of C & [(g `2),(f `2)] in dom the Comp of D ) by A1;

hence [gg,ff] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A7, FUNCT_4:54; :: thesis: verum

( [g,f] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) iff dom g = cod f ) by A6;

A11: for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds

|: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))]

proof

A13:
for f, g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f holds
let f, g be Element of [: the carrier' of C, the carrier' of D:]; :: thesis: ( [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f implies |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] )

reconsider ff = f, gg = g as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;

assume [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; :: thesis: |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))]

then A12: dom gg = cod ff ;

( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;

hence |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] by A12, A10, FUNCT_4:55; :: thesis: verum

end;reconsider ff = f, gg = g as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;

assume [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; :: thesis: |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))]

then A12: dom gg = cod ff ;

( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;

hence |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] by A12, A10, FUNCT_4:55; :: thesis: verum

( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g )

proof

A32:
CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is transitive
let f, g be Element of [: the carrier' of C, the carrier' of D:]; :: thesis: ( [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f implies ( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g ) )

reconsider ff = f, gg = g as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;

A14: ( f = [(f `1),(f `2)] & [: the Source of C, the Source of D:] . ((f `1),(f `2)) = [(dom (f `1)),(dom (f `2))] ) by FUNCT_3:75, MCART_1:21;

assume A15: [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; :: thesis: ( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g )

then A16: the Comp of C . [(g `1),(f `1)] in the carrier' of C by A1, PARTFUN1:4;

then A17: the Comp of C . ((g `1),(f `1)) in dom the Source of C by FUNCT_2:def 1;

dom gg = cod ff by A15;

then A18: [gg,ff] in dom |: the Comp of C, the Comp of D:| by A6;

then A19: dom (g `1) = cod (f `1) by A4;

then [(g `1),(f `1)] in dom the Comp of C by CAT_1:def 6;

then A20: the Comp of C . ((g `1),(f `1)) = (g `1) (*) (f `1) by CAT_1:def 1;

A21: dom ((g `1) (*) (f `1)) = dom (f `1) by A19, CAT_1:def 7;

A22: the Comp of D . [(g `2),(f `2)] in the carrier' of D by A1, A15, PARTFUN1:4;

then A23: the Comp of D . ((g `2),(f `2)) in dom the Source of D by FUNCT_2:def 1;

A24: dom (g `2) = cod (f `2) by A4, A18;

then [(g `2),(f `2)] in dom the Comp of D by CAT_1:def 6;

then A25: the Comp of D . ((g `2),(f `2)) = (g `2) (*) (f `2) by CAT_1:def 1;

A26: dom ((g `2) (*) (f `2)) = dom (f `2) by A24, CAT_1:def 7;

thus [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . (( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))) by A11, A15

.= [: the Source of C, the Source of D:] . f by A14, A21, A26, A17, A23, A20, A25, FUNCT_3:def 8 ; :: thesis: [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g

A27: ( g = [(g `1),(g `2)] & [: the Target of C, the Target of D:] . ((g `1),(g `2)) = [( the Target of C . (g `1)),( the Target of D . (g `2))] ) by FUNCT_3:75, MCART_1:21;

A28: cod ((g `2) (*) (f `2)) = cod (g `2) by A24, CAT_1:def 7;

A29: cod ((g `1) (*) (f `1)) = cod (g `1) by A19, CAT_1:def 7;

A30: the Comp of D . ((g `2),(f `2)) in dom the Target of D by A22, FUNCT_2:def 1;

A31: the Comp of C . ((g `1),(f `1)) in dom the Target of C by A16, FUNCT_2:def 1;

thus [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . (( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))) by A11, A15

.= [: the Target of C, the Target of D:] . g by A27, A29, A28, A31, A30, A20, A25, FUNCT_3:def 8 ; :: thesis: verum

end;reconsider ff = f, gg = g as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;

A14: ( f = [(f `1),(f `2)] & [: the Source of C, the Source of D:] . ((f `1),(f `2)) = [(dom (f `1)),(dom (f `2))] ) by FUNCT_3:75, MCART_1:21;

assume A15: [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; :: thesis: ( [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . f & [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g )

then A16: the Comp of C . [(g `1),(f `1)] in the carrier' of C by A1, PARTFUN1:4;

then A17: the Comp of C . ((g `1),(f `1)) in dom the Source of C by FUNCT_2:def 1;

dom gg = cod ff by A15;

then A18: [gg,ff] in dom |: the Comp of C, the Comp of D:| by A6;

then A19: dom (g `1) = cod (f `1) by A4;

then [(g `1),(f `1)] in dom the Comp of C by CAT_1:def 6;

then A20: the Comp of C . ((g `1),(f `1)) = (g `1) (*) (f `1) by CAT_1:def 1;

A21: dom ((g `1) (*) (f `1)) = dom (f `1) by A19, CAT_1:def 7;

A22: the Comp of D . [(g `2),(f `2)] in the carrier' of D by A1, A15, PARTFUN1:4;

then A23: the Comp of D . ((g `2),(f `2)) in dom the Source of D by FUNCT_2:def 1;

A24: dom (g `2) = cod (f `2) by A4, A18;

then [(g `2),(f `2)] in dom the Comp of D by CAT_1:def 6;

then A25: the Comp of D . ((g `2),(f `2)) = (g `2) (*) (f `2) by CAT_1:def 1;

A26: dom ((g `2) (*) (f `2)) = dom (f `2) by A24, CAT_1:def 7;

thus [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Source of C, the Source of D:] . (( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))) by A11, A15

.= [: the Source of C, the Source of D:] . f by A14, A21, A26, A17, A23, A20, A25, FUNCT_3:def 8 ; :: thesis: [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . g

A27: ( g = [(g `1),(g `2)] & [: the Target of C, the Target of D:] . ((g `1),(g `2)) = [( the Target of C . (g `1)),( the Target of D . (g `2))] ) by FUNCT_3:75, MCART_1:21;

A28: cod ((g `2) (*) (f `2)) = cod (g `2) by A24, CAT_1:def 7;

A29: cod ((g `1) (*) (f `1)) = cod (g `1) by A19, CAT_1:def 7;

A30: the Comp of D . ((g `2),(f `2)) in dom the Target of D by A22, FUNCT_2:def 1;

A31: the Comp of C . ((g `1),(f `1)) in dom the Target of C by A16, FUNCT_2:def 1;

thus [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) = [: the Target of C, the Target of D:] . (( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))) by A11, A15

.= [: the Target of C, the Target of D:] . g by A27, A29, A28, A31, A30, A20, A25, FUNCT_3:def 8 ; :: thesis: verum

proof

A35:
CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is associative
let ff, gg be Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: 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 Element of [: the carrier' of C, the carrier' of D:] ;

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

then A34: the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) . (gg,ff) = gg (*) ff by A10, CAT_1:def 1;

thus dom (gg (*) ff) = dom ff by A13, A33, A34; :: thesis: cod (gg (*) ff) = cod gg

thus cod (gg (*) ff) = cod gg by A13, A33, A34; :: thesis: verum

end;reconsider f = ff, g = gg as Element of [: the carrier' of C, the carrier' of D:] ;

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

then A34: the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) . (gg,ff) = gg (*) ff by A10, CAT_1:def 1;

thus dom (gg (*) ff) = dom ff by A13, A33, A34; :: thesis: cod (gg (*) ff) = cod gg

thus cod (gg (*) ff) = cod gg by A13, A33, A34; :: thesis: verum

proof

A62:
CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is reflexive
let ff, gg, hh be Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: 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 Element of [: the carrier' of C, the carrier' of D:] ;

assume that

A36: dom hh = cod gg and

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

A38: ( the Comp of C . [(h `1),(g `1)] in the carrier' of C & the Comp of D . [(h `2),(g `2)] in the carrier' of D ) by A1, A36, PARTFUN1:4;

( the Comp of C . [(g `1),(f `1)] in the carrier' of C & the Comp of D . [(g `2),(f `2)] in the carrier' of D ) by A1, A37, PARTFUN1:4;

then reconsider pgf = [( the Comp of C . [(g `1),(f `1)]),( the Comp of D . [(g `2),(f `2)])], phg = [( the Comp of C . [(h `1),(g `1)]),( the Comp of D . [(h `2),(g `2)])] as Element of [: the carrier' of C, the carrier' of D:] by A38, ZFMISC_1:87;

set pgf2 = pgf `2 ;

set phg2 = phg `2 ;

set pgf1 = pgf `1 ;

set phg1 = phg `1 ;

A39: |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] by A11, A37;

A40: [: the Source of C, the Source of D:] . h = [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) by A13, A36, A37;

A41: |: the Comp of C, the Comp of D:| . (h,g) = [( the Comp of C . ((h `1),(g `1))),( the Comp of D . ((h `2),(g `2)))] by A11, A36;

[(h `2),(g `2)] in dom the Comp of D by A1, A36;

then A42: dom (h `2) = cod (g `2) by CAT_1:def 6;

[(h `1),(g `1)] in dom the Comp of C by A1, A36;

then A43: dom (h `1) = cod (g `1) by CAT_1:def 6;

[(g `2),(f `2)] in dom the Comp of D by A1, A37;

then A44: dom (g `2) = cod (f `2) by CAT_1:def 6;

[(g `1),(f `1)] in dom the Comp of C by A1, A37;

then A45: dom (g `1) = cod (f `1) by CAT_1:def 6;

A46: [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (h,g)) = [: the Target of C, the Target of D:] . f by A13, A36, A37;

A47: ( pgf `1 = the Comp of C . ((g `1),(f `1)) & phg `1 = the Comp of C . ((h `1),(g `1)) ) ;

A48: ( pgf `2 = the Comp of D . ((g `2),(f `2)) & phg `2 = the Comp of D . ((h `2),(g `2)) ) ;

A49: (h `2) (*) ((g `2) (*) (f `2)) = ((h `2) (*) (g `2)) (*) (f `2) by A42, A44, CAT_1:def 8;

A50: gg (*) ff = |: the Comp of C, the Comp of D:| . (g,f) by A37, A10, CAT_1:def 1;

then A51: cod (gg (*) ff) = dom hh by A13, A36, A37;

A52: hh (*) gg = |: the Comp of C, the Comp of D:| . (h,g) by A36, A10, CAT_1:def 1;

then A53: dom (hh (*) gg) = cod ff by A13, A36, A37;

A54: cod ((g `1) (*) (f `1)) = cod (g `1) by A45, CAT_1:def 7;

A55: pgf `1 = (g `1) (*) (f `1) by A47, A45, CAT_1:16;

A56: cod ((g `2) (*) (f `2)) = cod (g `2) by A44, CAT_1:def 7;

pgf `2 = (g `2) (*) (f `2) by A48, A44, CAT_1:16;

then A57: the Comp of D . ((h `2),(pgf `2)) = (h `2) (*) ((g `2) (*) (f `2)) by A42, A56, CAT_1:16;

A58: dom ((h `1) (*) (g `1)) = dom (g `1) by A43, CAT_1:def 7;

A59: phg `1 = (h `1) (*) (g `1) by A47, A43, CAT_1:16;

A60: dom ((h `2) (*) (g `2)) = dom (g `2) by A42, CAT_1:def 7;

phg `2 = (h `2) (*) (g `2) by A48, A42, CAT_1:16;

then A61: the Comp of D . ((phg `2),(f `2)) = ((h `2) (*) (g `2)) (*) (f `2) by A44, A60, CAT_1:16;

thus hh (*) (gg (*) ff) = |: the Comp of C, the Comp of D:| . (h,(|: the Comp of C, the Comp of D:| . (g,f))) by A51, A50, A10, CAT_1:def 1

.= [( the Comp of C . ((h `1),(pgf `1))),( the Comp of D . ((h `2),(pgf `2)))] by A40, A11, A39

.= [((h `1) (*) ((g `1) (*) (f `1))),((h `2) (*) ((g `2) (*) (f `2)))] by A55, A57, A43, A54, CAT_1:16

.= [(((h `1) (*) (g `1)) (*) (f `1)),(((h `2) (*) (g `2)) (*) (f `2))] by A43, A45, A49, CAT_1:def 8

.= [( the Comp of C . ((phg `1),(f `1))),( the Comp of D . ((phg `2),(f `2)))] by A59, A61, A45, A58, CAT_1:16

.= |: the Comp of C, the Comp of D:| . ((|: the Comp of C, the Comp of D:| . (h,g)),f) by A46, A11, A41

.= (hh (*) gg) (*) ff by A53, A10, A52, CAT_1:def 1 ; :: thesis: verum

end;reconsider f = ff, g = gg, h = hh as Element of [: the carrier' of C, the carrier' of D:] ;

assume that

A36: dom hh = cod gg and

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

A38: ( the Comp of C . [(h `1),(g `1)] in the carrier' of C & the Comp of D . [(h `2),(g `2)] in the carrier' of D ) by A1, A36, PARTFUN1:4;

( the Comp of C . [(g `1),(f `1)] in the carrier' of C & the Comp of D . [(g `2),(f `2)] in the carrier' of D ) by A1, A37, PARTFUN1:4;

then reconsider pgf = [( the Comp of C . [(g `1),(f `1)]),( the Comp of D . [(g `2),(f `2)])], phg = [( the Comp of C . [(h `1),(g `1)]),( the Comp of D . [(h `2),(g `2)])] as Element of [: the carrier' of C, the carrier' of D:] by A38, ZFMISC_1:87;

set pgf2 = pgf `2 ;

set phg2 = phg `2 ;

set pgf1 = pgf `1 ;

set phg1 = phg `1 ;

A39: |: the Comp of C, the Comp of D:| . (g,f) = [( the Comp of C . ((g `1),(f `1))),( the Comp of D . ((g `2),(f `2)))] by A11, A37;

A40: [: the Source of C, the Source of D:] . h = [: the Target of C, the Target of D:] . (|: the Comp of C, the Comp of D:| . (g,f)) by A13, A36, A37;

A41: |: the Comp of C, the Comp of D:| . (h,g) = [( the Comp of C . ((h `1),(g `1))),( the Comp of D . ((h `2),(g `2)))] by A11, A36;

[(h `2),(g `2)] in dom the Comp of D by A1, A36;

then A42: dom (h `2) = cod (g `2) by CAT_1:def 6;

[(h `1),(g `1)] in dom the Comp of C by A1, A36;

then A43: dom (h `1) = cod (g `1) by CAT_1:def 6;

[(g `2),(f `2)] in dom the Comp of D by A1, A37;

then A44: dom (g `2) = cod (f `2) by CAT_1:def 6;

[(g `1),(f `1)] in dom the Comp of C by A1, A37;

then A45: dom (g `1) = cod (f `1) by CAT_1:def 6;

A46: [: the Source of C, the Source of D:] . (|: the Comp of C, the Comp of D:| . (h,g)) = [: the Target of C, the Target of D:] . f by A13, A36, A37;

A47: ( pgf `1 = the Comp of C . ((g `1),(f `1)) & phg `1 = the Comp of C . ((h `1),(g `1)) ) ;

A48: ( pgf `2 = the Comp of D . ((g `2),(f `2)) & phg `2 = the Comp of D . ((h `2),(g `2)) ) ;

A49: (h `2) (*) ((g `2) (*) (f `2)) = ((h `2) (*) (g `2)) (*) (f `2) by A42, A44, CAT_1:def 8;

A50: gg (*) ff = |: the Comp of C, the Comp of D:| . (g,f) by A37, A10, CAT_1:def 1;

then A51: cod (gg (*) ff) = dom hh by A13, A36, A37;

A52: hh (*) gg = |: the Comp of C, the Comp of D:| . (h,g) by A36, A10, CAT_1:def 1;

then A53: dom (hh (*) gg) = cod ff by A13, A36, A37;

A54: cod ((g `1) (*) (f `1)) = cod (g `1) by A45, CAT_1:def 7;

A55: pgf `1 = (g `1) (*) (f `1) by A47, A45, CAT_1:16;

A56: cod ((g `2) (*) (f `2)) = cod (g `2) by A44, CAT_1:def 7;

pgf `2 = (g `2) (*) (f `2) by A48, A44, CAT_1:16;

then A57: the Comp of D . ((h `2),(pgf `2)) = (h `2) (*) ((g `2) (*) (f `2)) by A42, A56, CAT_1:16;

A58: dom ((h `1) (*) (g `1)) = dom (g `1) by A43, CAT_1:def 7;

A59: phg `1 = (h `1) (*) (g `1) by A47, A43, CAT_1:16;

A60: dom ((h `2) (*) (g `2)) = dom (g `2) by A42, CAT_1:def 7;

phg `2 = (h `2) (*) (g `2) by A48, A42, CAT_1:16;

then A61: the Comp of D . ((phg `2),(f `2)) = ((h `2) (*) (g `2)) (*) (f `2) by A44, A60, CAT_1:16;

thus hh (*) (gg (*) ff) = |: the Comp of C, the Comp of D:| . (h,(|: the Comp of C, the Comp of D:| . (g,f))) by A51, A50, A10, CAT_1:def 1

.= [( the Comp of C . ((h `1),(pgf `1))),( the Comp of D . ((h `2),(pgf `2)))] by A40, A11, A39

.= [((h `1) (*) ((g `1) (*) (f `1))),((h `2) (*) ((g `2) (*) (f `2)))] by A55, A57, A43, A54, CAT_1:16

.= [(((h `1) (*) (g `1)) (*) (f `1)),(((h `2) (*) (g `2)) (*) (f `2))] by A43, A45, A49, CAT_1:def 8

.= [( the Comp of C . ((phg `1),(f `1))),( the Comp of D . ((phg `2),(f `2)))] by A59, A61, A45, A58, CAT_1:16

.= |: the Comp of C, the Comp of D:| . ((|: the Comp of C, the Comp of D:| . (h,g)),f) by A46, A11, A41

.= (hh (*) gg) (*) ff by A53, A10, A52, CAT_1:def 1 ; :: thesis: verum

proof

CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is with_identities
let b be Element of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: according to CAT_1:def 9 :: thesis: not Hom (b,b) = {}

reconsider bb = b as Element of [: the carrier of C, the carrier of D:] ;

reconsider ii = [(id (bb `1)),(id (bb `2))] as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;

A63: cod ii = [: the Target of C, the Target of D:] . ((id (bb `1)),(id (bb `2)))

.= [(cod (id (bb `1))),(cod (id (bb `2)))] by FUNCT_3:75

.= [(bb `1),(cod (id (bb `2)))]

.= [(bb `1),(bb `2)]

.= bb by MCART_1:21 ;

dom ii = [: the Source of C, the Source of D:] . ((id (bb `1)),(id (bb `2)))

.= [(dom (id (bb `1))),(dom (id (bb `2)))] by FUNCT_3:75

.= [(bb `1),(dom (id (bb `2)))]

.= [(bb `1),(bb `2)]

.= bb by MCART_1:21 ;

then [(id (bb `1)),(id (bb `2))] in Hom (b,b) by A63;

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

end;reconsider bb = b as Element of [: the carrier of C, the carrier of D:] ;

reconsider ii = [(id (bb `1)),(id (bb `2))] as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;

A63: cod ii = [: the Target of C, the Target of D:] . ((id (bb `1)),(id (bb `2)))

.= [(cod (id (bb `1))),(cod (id (bb `2)))] by FUNCT_3:75

.= [(bb `1),(cod (id (bb `2)))]

.= [(bb `1),(bb `2)]

.= bb by MCART_1:21 ;

dom ii = [: the Source of C, the Source of D:] . ((id (bb `1)),(id (bb `2)))

.= [(dom (id (bb `1))),(dom (id (bb `2)))] by FUNCT_3:75

.= [(bb `1),(dom (id (bb `2)))]

.= [(bb `1),(bb `2)]

.= bb by MCART_1:21 ;

then [(id (bb `1)),(id (bb `2))] in Hom (b,b) by A63;

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

proof

hence
CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category
by A6, A32, A35, A62; :: thesis: verum
let a be Element of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: 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(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) 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 [: the carrier of C, the carrier of D:] ;

reconsider ii = [(id (aa `1)),(id (aa `2))] as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;

A64: cod ii = [: the Target of C, the Target of D:] . ((id (aa `1)),(id (aa `2)))

.= [(cod (id (aa `1))),(cod (id (aa `2)))] by FUNCT_3:75

.= [(aa `1),(cod (id (aa `2)))]

.= [(aa `1),(aa `2)]

.= aa by MCART_1:21 ;

A65: dom ii = [: the Source of C, the Source of D:] . ((id (aa `1)),(id (aa `2)))

.= [(dom (id (aa `1))),(dom (id (aa `2)))] by FUNCT_3:75

.= [(aa `1),(dom (id (aa `2)))]

.= [(aa `1),(aa `2)]

.= aa by MCART_1:21 ;

then reconsider ii = [(id (aa `1)),(id (aa `2))] as Morphism of a,a by A64, CAT_1:4;

take ii ; :: thesis: for b_{1} being Element of the carrier of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) 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(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: 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 [: the carrier' of C, the carrier' of D:] ;

dom ii = cod g by A73, A65, CAT_1:5;

then A74: [ii,g] in dom |: the Comp of C, the Comp of D:| by A6;

then A75: cod (gg `1) = dom ([(id (aa `1)),(id (aa `2))] `1) by A4

.= dom (id (aa `1)) ;

A76: the Comp of C . ((id (aa `1)),(gg `1)) = (id (aa `1)) (*) (gg `1) by A75, CAT_1:16

.= gg `1 by A75, CAT_1:21 ;

A77: cod (gg `2) = dom ([(id (aa `1)),(id (aa `2))] `2) by A4, A74

.= dom (id (aa `2)) ;

A78: the Comp of D . ((id (aa `2)),(gg `2)) = (id (aa `2)) (*) (gg `2) by A77, CAT_1:16

.= gg `2 by A77, CAT_1:21 ;

A79: dom ii = cod g by A65, A73, CAT_1:5;

then [ii,g] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A6;

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

.= [( the Comp of C . (([(id (aa `1)),(id (aa `2))] `1),(gg `1))),( the Comp of D . (([(id (aa `1)),(id (aa `2))] `2),(gg `2)))] by A11, A79

.= g by A76, A78, MCART_1:21 ;

:: thesis: verum

end;for b

( ( Hom (a,b

reconsider aa = a as Element of [: the carrier of C, the carrier of D:] ;

reconsider ii = [(id (aa `1)),(id (aa `2))] as Morphism of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) ;

A64: cod ii = [: the Target of C, the Target of D:] . ((id (aa `1)),(id (aa `2)))

.= [(cod (id (aa `1))),(cod (id (aa `2)))] by FUNCT_3:75

.= [(aa `1),(cod (id (aa `2)))]

.= [(aa `1),(aa `2)]

.= aa by MCART_1:21 ;

A65: dom ii = [: the Source of C, the Source of D:] . ((id (aa `1)),(id (aa `2)))

.= [(dom (id (aa `1))),(dom (id (aa `2)))] by FUNCT_3:75

.= [(aa `1),(dom (id (aa `2)))]

.= [(aa `1),(aa `2)]

.= aa by MCART_1:21 ;

then reconsider ii = [(id (aa `1)),(id (aa `2))] as Morphism of a,a by A64, CAT_1:4;

take ii ; :: thesis: for b

( ( Hom (a,b

let b be Element of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #); :: 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 A73:
Hom (b,a) <> {}
; :: thesis: for b
assume A66:
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 [: the carrier' of C, the carrier' of D:] ;

cod ii = dom g by A66, A64, CAT_1:5;

then A67: [g,ii] in dom |: the Comp of C, the Comp of D:| by A6;

then A68: dom (gg `1) = cod ([(id (aa `1)),(id (aa `2))] `1) by A4

.= cod (id (aa `1)) ;

A69: the Comp of C . ((gg `1),(id (aa `1))) = (gg `1) (*) (id (aa `1)) by A68, CAT_1:16

.= gg `1 by A68, CAT_1:22 ;

A70: dom (gg `2) = cod ([(id (aa `1)),(id (aa `2))] `2) by A4, A67

.= cod (id (aa `2)) ;

A71: the Comp of D . ((gg `2),(id (aa `2))) = (gg `2) (*) (id (aa `2)) by A70, CAT_1:16

.= gg `2 by A70, CAT_1:22 ;

A72: cod ii = dom g by A64, A66, CAT_1:5;

then [g,ii] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A6;

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

.= [( the Comp of C . ((gg `1),([(id (aa `1)),(id (aa `2))] `1))),( the Comp of D . ((gg `2),([(id (aa `1)),(id (aa `2))] `2)))] by A11, A72

.= g by A69, A71, MCART_1:21 ;

:: thesis: verum

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

reconsider gg = g as Element of [: the carrier' of C, the carrier' of D:] ;

cod ii = dom g by A66, A64, CAT_1:5;

then A67: [g,ii] in dom |: the Comp of C, the Comp of D:| by A6;

then A68: dom (gg `1) = cod ([(id (aa `1)),(id (aa `2))] `1) by A4

.= cod (id (aa `1)) ;

A69: the Comp of C . ((gg `1),(id (aa `1))) = (gg `1) (*) (id (aa `1)) by A68, CAT_1:16

.= gg `1 by A68, CAT_1:22 ;

A70: dom (gg `2) = cod ([(id (aa `1)),(id (aa `2))] `2) by A4, A67

.= cod (id (aa `2)) ;

A71: the Comp of D . ((gg `2),(id (aa `2))) = (gg `2) (*) (id (aa `2)) by A70, CAT_1:16

.= gg `2 by A70, CAT_1:22 ;

A72: cod ii = dom g by A64, A66, CAT_1:5;

then [g,ii] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A6;

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

.= [( the Comp of C . ((gg `1),([(id (aa `1)),(id (aa `2))] `1))),( the Comp of D . ((gg `2),([(id (aa `1)),(id (aa `2))] `2)))] by A11, A72

.= g by A69, A71, MCART_1:21 ;

:: thesis: verum

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

reconsider gg = g as Element of [: the carrier' of C, the carrier' of D:] ;

dom ii = cod g by A73, A65, CAT_1:5;

then A74: [ii,g] in dom |: the Comp of C, the Comp of D:| by A6;

then A75: cod (gg `1) = dom ([(id (aa `1)),(id (aa `2))] `1) by A4

.= dom (id (aa `1)) ;

A76: the Comp of C . ((id (aa `1)),(gg `1)) = (id (aa `1)) (*) (gg `1) by A75, CAT_1:16

.= gg `1 by A75, CAT_1:21 ;

A77: cod (gg `2) = dom ([(id (aa `1)),(id (aa `2))] `2) by A4, A74

.= dom (id (aa `2)) ;

A78: the Comp of D . ((id (aa `2)),(gg `2)) = (id (aa `2)) (*) (gg `2) by A77, CAT_1:16

.= gg `2 by A77, CAT_1:21 ;

A79: dom ii = cod g by A65, A73, CAT_1:5;

then [ii,g] in dom the Comp of CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) by A6;

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

.= [( the Comp of C . (([(id (aa `1)),(id (aa `2))] `1),(gg `1))),( the Comp of D . (([(id (aa `1)),(id (aa `2))] `2),(gg `2)))] by A11, A79

.= g by A76, A78, MCART_1:21 ;

:: thesis: verum