let C1, C2 be strict Category; :: thesis:
assume that
A127: the carrier of C1 = Funct (A,B) and
A128: the carrier' of C1 = NatTrans (A,B) and
A129: for f being Morphism of C1 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) and
A130: for f, g being Morphism of C1 st dom g = cod f holds
[g,f] in dom the Comp of C1 and
A131: for f, g being Morphism of C1 st [g,f] in dom the Comp of C1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] ) and
for a being Object of C1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] and
A132: the carrier of C2 = Funct (A,B) and
A133: the carrier' of C2 = NatTrans (A,B) and
A134: for f being Morphism of C2 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) and
A135: for f, g being Morphism of C2 st dom g = cod f holds
[g,f] in dom the Comp of C2 and
A136: for f, g being Morphism of C2 st [g,f] in dom the Comp of C2 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C2 . [g,f] = [[F,F2],(t1 `*` t)] ) and
for a being Object of C2
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ; :: thesis:
A137: the Target of C1 = the Target of C2

thus the carrier' of C1 = the carrier' of C2 by A128, A133; :: according to FUNCT_2:def 7 :: thesis:
let a be Morphism of C1; :: thesis:
reconsider b = a as Morphism of C2 by A128, A133;
thus the Target of C1 . a = cod a
.= (a `1) `2 by A129
.= cod b by A134
.= the Target of C2 . a ; :: thesis:

end;

reconsider S1 = dom the Comp of C1, S2 = dom the Comp of C2 as Subset of [: the carrier' of C1, the carrier' of C1:] by A128, A133, RELAT_1:def 18;

let x be Element of [: the carrier' of C1, the carrier' of C1:]; :: thesis:
A140: x = [(x `1),(x `2)] by MCART_1:21;
then reconsider f1 = x `2 , g1 = x `1 as Morphism of C1 by ZFMISC_1:87;
reconsider f2 = x `2 , g2 = x `1 as Morphism of C2 by A128, A133, A140, ZFMISC_1:87;

assume [g2,f2] in S2 ; :: thesis:
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A142: f2 = [[F,F1],t] and
A143: g2 = [[F1,F2],t1] and
the Comp of C2 . [g2,f2] = [[F,F2],(t1 `*` t)] by A136;
dom g1 = (g1 `1) `1 by A129
.= [F1,F2] `1 by A143
.= [F,F1] `2
.= (f2 `1) `2 by A142
.= cod f1 by A129 ;
hence [g1,f1] in S1 by A130; :: thesis:

end;

assume [g1,f1] in S1 ; :: thesis:
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A144: f1 = [[F,F1],t] and
A145: g1 = [[F1,F2],t1] and
the Comp of C1 . [g1,f1] = [[F,F2],(t1 `*` t)] by A131;
dom g2 = (g2 `1) `1 by A134
.= [F1,F2] `1 by A145
.= [F,F1] `2
.= (f1 `1) `2 by A144
.= cod f2 by A134 ;
hence [g2,f2] in S2 by A135; :: thesis:

end;

end;

hence dom the Comp of C1 = dom the Comp of C2 by SUBSET_1:3; :: thesis:
let x be object ; :: thesis:
assume A146: x in dom the Comp of C1 ; :: thesis:
dom the Comp of C1 c= [: the carrier' of C1, the carrier' of C1:] by RELAT_1:def 18;
then reconsider f = x `2 , g = x `1 as Morphism of C1 by A146, MCART_1:10;
A147: [g,f] = x by A146, MCART_1:21;
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A148: f = [[F9,F19],t9] and
A149: g = [[F19,F29],t19] and
A150: the Comp of C2 . [g,f] = [[F9,F29],(t19 `*` t9)] by A128, A133, A136, A139, A146;
consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A151: f = [[F,F1],t] and
A152: g = [[F1,F2],t1] and
A153: the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] by A131, A146, A147;
A154: [F,F1] = [F9,F19] by A151, A148, XTUPLE_0:1;
then A155: F = F9 by XTUPLE_0:1;
[F1,F2] = [F19,F29] by A152, A149, XTUPLE_0:1;
then A156: F2 = F29 by XTUPLE_0:1;
A157: F1 = F19 by A154, XTUPLE_0:1;
t = t9 by A151, A148, XTUPLE_0:1;
hence the Comp of C1 . x = the Comp of C2 . x by A147, A152, A153, A149, A150, A155, A157, A156, XTUPLE_0:1; :: thesis:

end;

the Source of C1 = the Source of C2

thus the carrier' of C1 = the carrier' of C2 by A128, A133; :: according to FUNCT_2:def 7 :: thesis:
let a be Morphism of C1; :: thesis:
reconsider b = a as Morphism of C2 by A128, A133;
thus the Source of C1 . a = dom a
.= (a `1) `1 by A129
.= dom b by A134
.= the Source of C2 . a ; :: thesis:

end;