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:|;
set i = [: the Id of C, the Id 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 ( the Source of C . (g `1) = the Target of C . (f `1) & the Source of D . (g `2) = the Target of D . (f `2) ) by A2, A3, ZFMISC_1:27;
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 5; :: 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
( the Source of C . (g `1) = the Target of C . (f `1) & the Source of D . (g `2) = the Target of D . (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 ( the Source of C . (g `1) = the Target of C . (f `1) & the Source of D . (g `2) = the Target of D . (f `2) ) )
assume A5: [g,f] in dom |: the Comp of C, the Comp of D:| ; :: thesis: ( the Source of C . (g `1) = the Target of C . (f `1) & the Source of D . (g `2) = the Target of D . (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 ( the Source of C . (g `1) = the Target of C . (f `1) & the Source of D . (g `2) = the Target of D . (f `2) ) by CAT_1:def 5; :: thesis: verum

end;

A6: for f, g being Element of [: the carrier' of C, the carrier' of D:] holds
( [g,f] in dom |: the Comp of C, the Comp of D:| iff [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f )

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:| iff [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f )
A7: ( g = [(g `1),(g `2)] & f = [(f `1),(f `2)] ) by MCART_1:21;
thus ( [g,f] in dom |: the Comp of C, the Comp of D:| implies [: 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:] . g = [: the Target of C, the Target of D:] . f implies [g,f] in dom |: the Comp of C, the Comp of D:| )

proof

A8: ( [: 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 A9: [g,f] in dom |: the Comp of C, the Comp of D:| ; :: thesis: [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f
then the Source of C . (g `1) = the Target of C . (f `1) by A4;
hence [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f by A4, A7, A9, A8; :: thesis: verum

end;

assume [: the Source of C, the Source of D:] . g = [: the Target of C, the Target of D:] . f ; :: thesis: [g,f] in dom |: 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 [g,f] in dom |: the Comp of C, the Comp of D:| by A7, FUNCT_4:54; :: thesis: verum

end;

A10: 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)))] )
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 A11: [g,f] in dom |: the Comp of C, the Comp of D:| by A6;
( 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 A11, FUNCT_4:55; :: thesis: verum

end;

A12: now

let b be Element of [: the carrier of C, the carrier of D:]; :: thesis: ( [: the Source of C, the Source of D:] . ([: the Id of C, the Id of D:] . b) = b & [: the Target of C, the Target of D:] . ([: the Id of C, the Id of D:] . b) = b & ( for f being Element of [: the carrier' of C, the carrier' of D:] st [: the Target of C, the Target of D:] . f = b holds
|: the Comp of C, the Comp of D:| . (([: the Id of C, the Id of D:] . b),f) = f ) & ( for g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = b holds
|: the Comp of C, the Comp of D:| . (g,([: the Id of C, the Id of D:] . b)) = g ) )
A13: b = [(b `1),(b `2)] by MCART_1:21;
A14: ( the Source of C . ( the Id of C . (b `1)) = b `1 & the Source of D . ( the Id of D . (b `2)) = b `2 ) by CAT_1:def 5;
A15: [: the Id of C, the Id of D:] . ((b `1),(b `2)) = [( the Id of C . (b `1)),( the Id of D . (b `2))] by FUNCT_3:75;
hence A16: [: the Source of C, the Source of D:] . ([: the Id of C, the Id of D:] . b) = [: the Source of C, the Source of D:] . (( the Id of C . (b `1)),( the Id of D . (b `2))) by MCART_1:21
.= b by A13, A14, FUNCT_3:75 ;
:: thesis: ( [: the Target of C, the Target of D:] . ([: the Id of C, the Id of D:] . b) = b & ( for f being Element of [: the carrier' of C, the carrier' of D:] st [: the Target of C, the Target of D:] . f = b holds
|: the Comp of C, the Comp of D:| . (([: the Id of C, the Id of D:] . b),f) = f ) & ( for g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = b holds
|: the Comp of C, the Comp of D:| . (g,([: the Id of C, the Id of D:] . b)) = g ) )
A17: ( the Target of C . ( the Id of C . (b `1)) = b `1 & the Target of D . ( the Id of D . (b `2)) = b `2 ) by CAT_1:def 5;
thus A18: [: the Target of C, the Target of D:] . ([: the Id of C, the Id of D:] . b) = [: the Target of C, the Target of D:] . (( the Id of C . (b `1)),( the Id of D . (b `2))) by A15, MCART_1:21
.= b by A13, A17, FUNCT_3:75 ; :: thesis: ( ( for f being Element of [: the carrier' of C, the carrier' of D:] st [: the Target of C, the Target of D:] . f = b holds
|: the Comp of C, the Comp of D:| . (([: the Id of C, the Id of D:] . b),f) = f ) & ( for g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = b holds
|: the Comp of C, the Comp of D:| . (g,([: the Id of C, the Id of D:] . b)) = g ) )
A19: ( ([: the Id of C, the Id of D:] . ((b `1),(b `2))) `1 = the Id of C . (b `1) & ([: the Id of C, the Id of D:] . ((b `1),(b `2))) `2 = the Id of D . (b `2) ) by A15, MCART_1:7;
thus for f being Element of [: the carrier' of C, the carrier' of D:] st [: the Target of C, the Target of D:] . f = b holds
|: the Comp of C, the Comp of D:| . (([: the Id of C, the Id of D:] . b),f) = f :: thesis: for g being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . g = b holds
|: the Comp of C, the Comp of D:| . (g,([: the Id of C, the Id of D:] . b)) = g

proof

let f be Element of [: the carrier' of C, the carrier' of D:]; :: thesis: ( [: the Target of C, the Target of D:] . f = b implies |: the Comp of C, the Comp of D:| . (([: the Id of C, the Id of D:] . b),f) = f )
assume A20: [: the Target of C, the Target of D:] . f = b ; :: thesis: |: the Comp of C, the Comp of D:| . (([: the Id of C, the Id of D:] . b),f) = f
A21: ( f = [(f `1),(f `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, MCART_1:21;
then the Target of C . (f `1) = b `1 by A13, A20, ZFMISC_1:27;
then A22: the Comp of C . (( the Id of C . (b `1)),(f `1)) = f `1 by CAT_1:def 5;
the Target of D . (f `2) = b `2 by A13, A20, A21, ZFMISC_1:27;
then A23: the Comp of D . (( the Id of D . (b `2)),(f `2)) = f `2 by CAT_1:def 5;
|: the Comp of C, the Comp of D:| . (([: the Id of C, the Id of D:] . ((b `1),(b `2))),f) = [( the Comp of C . ((([: the Id of C, the Id of D:] . b) `1),(f `1))),( the Comp of D . ((([: the Id of C, the Id of D:] . b) `2),(f `2)))] by A10, A13, A16, A20;
hence |: the Comp of C, the Comp of D:| . (([: the Id of C, the Id of D:] . b),f) = f by A13, A19, A22, A23, MCART_1:21; :: thesis: verum

end;

let g be Element of [: the carrier' of C, the carrier' of D:]; :: thesis: ( [: the Source of C, the Source of D:] . g = b implies |: the Comp of C, the Comp of D:| . (g,([: the Id of C, the Id of D:] . b)) = g )
assume A24: [: the Source of C, the Source of D:] . g = b ; :: thesis: |: the Comp of C, the Comp of D:| . (g,([: the Id of C, the Id of D:] . b)) = g
A25: ( g = [(g `1),(g `2)] & [: the Source of C, the Source of D:] . ((g `1),(g `2)) = [( the Source of C . (g `1)),( the Source of D . (g `2))] ) by FUNCT_3:75, MCART_1:21;
then the Source of C . (g `1) = b `1 by A13, A24, ZFMISC_1:27;
then A26: the Comp of C . ((g `1),( the Id of C . (b `1))) = g `1 by CAT_1:def 5;
the Source of D . (g `2) = b `2 by A13, A24, A25, ZFMISC_1:27;
then A27: the Comp of D . ((g `2),( the Id of D . (b `2))) = g `2 by CAT_1:def 5;
|: the Comp of C, the Comp of D:| . (g,([: the Id of C, the Id of D:] . ((b `1),(b `2)))) = [( the Comp of C . ((g `1),(([: the Id of C, the Id of D:] . b) `1))),( the Comp of D . ((g `2),(([: the Id of C, the Id of D:] . b) `2)))] by A10, A13, A18, A24;
hence |: the Comp of C, the Comp of D:| . (g,([: the Id of C, the Id of D:] . b)) = g by A13, A19, A26, A27, MCART_1:21; :: thesis: verum

end;

A28: 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 ) )
A29: ( f = [(f `1),(f `2)] & [: the Source of C, the Source of D:] . ((f `1),(f `2)) = [( the Source of C . (f `1)),( the Source of D . (f `2))] ) by FUNCT_3:75, MCART_1:21;
assume A30: [: 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 A31: the Comp of C . [(g `1),(f `1)] in the carrier' of C by A1, PARTFUN1:4;
then A32: the Comp of C . ((g `1),(f `1)) in dom the Source of C by FUNCT_2:def 1;
A33: [g,f] in dom |: the Comp of C, the Comp of D:| by A6, A30;
then A34: the Source of C . (g `1) = the Target of C . (f `1) by A4;
then A35: the Source of C . ( the Comp of C . ((g `1),(f `1))) = the Source of C . (f `1) by CAT_1:def 5;
A36: the Comp of D . [(g `2),(f `2)] in the carrier' of D by A1, A30, PARTFUN1:4;
then A37: the Comp of D . ((g `2),(f `2)) in dom the Source of D by FUNCT_2:def 1;
A38: the Source of D . (g `2) = the Target of D . (f `2) by A4, A33;
then A39: the Source of D . ( the Comp of D . ((g `2),(f `2))) = the Source of D . (f `2) by CAT_1:def 5;
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 A10, A30
.= [: the Source of C, the Source of D:] . f by A29, A35, A39, A32, A37, 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
A40: ( 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;
A41: the Target of D . ( the Comp of D . ((g `2),(f `2))) = the Target of D . (g `2) by A38, CAT_1:def 5;
A42: the Target of C . ( the Comp of C . ((g `1),(f `1))) = the Target of C . (g `1) by A34, CAT_1:def 5;
A43: the Comp of D . ((g `2),(f `2)) in dom the Target of D by A36, FUNCT_2:def 1;
A44: the Comp of C . ((g `1),(f `1)) in dom the Target of C by A31, 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 A10, A30
.= [: the Target of C, the Target of D:] . g by A40, A42, A41, A44, A43, FUNCT_3:def 8 ; :: thesis: verum

end;

for f, g, h being Element of [: the carrier' of C, the carrier' of D:] st [: the Source of C, the Source of D:] . h = [: the Target of C, the Target of D:] . g & [: 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:| . (h,(|: the Comp of C, the Comp of D:| . (g,f))) = |: the Comp of C, the Comp of D:| . ((|: the Comp of C, the Comp of D:| . (h,g)),f)

proof

let f, g, h be Element of [: the carrier' of C, the carrier' of D:]; :: thesis: ( [: the Source of C, the Source of D:] . h = [: the Target of C, the Target of D:] . g & [: 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:| . (h,(|: the Comp of C, the Comp of D:| . (g,f))) = |: the Comp of C, the Comp of D:| . ((|: the Comp of C, the Comp of D:| . (h,g)),f) )
assume that
A45: [: the Source of C, the Source of D:] . h = [: the Target of C, the Target of D:] . g and
A46: [: 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:| . (h,(|: the Comp of C, the Comp of D:| . (g,f))) = |: the Comp of C, the Comp of D:| . ((|: the Comp of C, the Comp of D:| . (h,g)),f)
A47: ( 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, A45, 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, A46, 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 A47, ZFMISC_1:87;
set pgf2 = pgf `2 ;
set phg2 = phg `2 ;
set pgf1 = pgf `1 ;
set phg1 = phg `1 ;
A48: ( pgf `2 = the Comp of D . [(g `2),(f `2)] & phg `2 = the Comp of D . [(h `2),(g `2)] ) by MCART_1:7;
A49: |: 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 A10, A46;
[: 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 A28, A45, A46;
then A50: |: the Comp of C, the Comp of D:| . (h,(|: the Comp of C, the Comp of D:| . (g,f))) = [( the Comp of C . ((h `1),(pgf `1))),( the Comp of D . ((h `2),(pgf `2)))] by A10, A49;
A51: |: 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 A10, A45;
[(h `2),(g `2)] in dom the Comp of D by A1, A45;
then A52: the Source of D . (h `2) = the Target of D . (g `2) by CAT_1:def 5;
[(h `1),(g `1)] in dom the Comp of C by A1, A45;
then A53: the Source of C . (h `1) = the Target of C . (g `1) by CAT_1:def 5;
[(g `2),(f `2)] in dom the Comp of D by A1, A46;
then A54: the Source of D . (g `2) = the Target of D . (f `2) by CAT_1:def 5;
[(g `1),(f `1)] in dom the Comp of C by A1, A46;
then A55: the Source of C . (g `1) = the Target of C . (f `1) by CAT_1:def 5;
[: 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 A28, A45, A46;
then A56: |: the Comp of C, the Comp of D:| . ((|: the Comp of C, the Comp of D:| . (h,g)),f) = [( the Comp of C . ((phg `1),(f `1))),( the Comp of D . ((phg `2),(f `2)))] by A10, A51;
( pgf `1 = the Comp of C . [(g `1),(f `1)] & phg `1 = the Comp of C . [(h `1),(g `1)] ) by MCART_1:7;
then the Comp of C . ((h `1),(pgf `1)) = the Comp of C . ((phg `1),(f `1)) by A55, A53, A49, A51, CAT_1:def 5;
hence |: the Comp of C, the Comp of D:| . (h,(|: the Comp of C, the Comp of D:| . (g,f))) = |: the Comp of C, the Comp of D:| . ((|: the Comp of C, the Comp of D:| . (h,g)),f) by A48, A54, A52, A49, A51, A50, A56, CAT_1:def 5; :: 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:|,[: the Id of C, the Id of D:] #) is Category by A6, A28, A12, CAT_1:def 5; :: thesis: verum