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:
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:96;
assume A3: [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f ; :: thesis:
( g = [(g `1 ),(g `2 )] & f = [(f `1 ),(f `2 )] ) by MCART_1:23;
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:33;
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 8; :: thesis:

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:
assume A5: [g,f] in dom |:the Comp of C,the Comp of D:| ; :: thesis:
( g = [(g `1 ),(g `2 )] & f = [(f `1 ),(f `2 )] ) by MCART_1:23;
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:57;
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 8; :: thesis:

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:
A7: ( g = [(g `1 ),(g `2 )] & f = [(f `1 ),(f `2 )] ) by MCART_1:23;
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:

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:96;
assume A9: [g,f] in dom |:the Comp of C,the Comp of D:| ; :: thesis:
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:

end;

assume [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f ; :: thesis:
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:57; :: thesis:

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:
assume [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f ; :: thesis:
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:23;
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:58; :: thesis:

end;

A12: now

let b be Element of [:the carrier of C,the carrier of D:]; :: thesis:
A13: b = [(b `1 ),(b `2 )] by MCART_1:23;
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 8;
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:96;
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:23
.= b by A13, A14, FUNCT_3:96 ;
:: thesis:
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 8;
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:23
.= b by A13, A17, FUNCT_3:96 ; :: thesis:
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:

proof

let f be Element of [:the carrier' of C,the carrier' of D:]; :: thesis:
assume A20: [:the Target of C,the Target of D:] . f = b ; :: thesis:
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:96, MCART_1:23;
then the Target of C . (f `1 ) = b `1 by A13, A20, ZFMISC_1:33;
then A22: the Comp of C . (the Id of C . (b `1 )),(f `1 ) = f `1 by CAT_1:def 8;
the Target of D . (f `2 ) = b `2 by A13, A20, A21, ZFMISC_1:33;
then A23: the Comp of D . (the Id of D . (b `2 )),(f `2 ) = f `2 by CAT_1:def 8;
|: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:23; :: thesis:

end;

let g be Element of [:the carrier' of C,the carrier' of D:]; :: thesis:
assume A24: [:the Source of C,the Source of D:] . g = b ; :: thesis:
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:96, MCART_1:23;
then the Source of C . (g `1 ) = b `1 by A13, A24, ZFMISC_1:33;
then A26: the Comp of C . (g `1 ),(the Id of C . (b `1 )) = g `1 by CAT_1:def 8;
the Source of D . (g `2 ) = b `2 by A13, A24, A25, ZFMISC_1:33;
then A27: the Comp of D . (g `2 ),(the Id of D . (b `2 )) = g `2 by CAT_1:def 8;
|: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:23; :: thesis:

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:
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:96, MCART_1:23;
assume A30: [:the Source of C,the Source of D:] . g = [:the Target of C,the Target of D:] . f ; :: thesis:
then A31: the Comp of C . [(g `1 ),(f `1 )] in the carrier' of C by A1, PARTFUN1:27;
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 8;
A36: the Comp of D . [(g `2 ),(f `2 )] in the carrier' of D by A1, A30, PARTFUN1:27;
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 8;
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 9 ; :: thesis:
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:96, MCART_1:23;
A41: the Target of D . (the Comp of D . (g `2 ),(f `2 )) = the Target of D . (g `2 ) by A38, CAT_1:def 8;
A42: the Target of C . (the Comp of C . (g `1 ),(f `1 )) = the Target of C . (g `1 ) by A34, CAT_1:def 8;
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 9 ; :: thesis:

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:
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:
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:27;
( 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:27;
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:106;
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 8;
[(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 8;
[(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 8;
[(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 8;
[: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 8;
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 8; :: thesis:

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 8; :: thesis: