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 )
proof
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;
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
( dom (g `1) = cod (f `1) & dom (g `2) = cod (f `2) )
proof
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;
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:| #);
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
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:| #) )
proof
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 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:| #)
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;
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
( [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
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;
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
( [: 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
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;
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
proof
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;
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
proof
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;
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
proof
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;
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
proof
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 b1 being Morphism of a,a st
for b2 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,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
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 b1 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,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
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 b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) :: thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )
proof
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;
assume A73: Hom (b,a) <> {} ; :: thesis: for b1 being Morphism of b,a holds ii (*) b1 = b1
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;
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