let C1, C2 be strict Category; :: thesis: ( the carrier of C1 = Funct A,B & the carrier' of C1 = NatTrans A,B & ( for f being Morphism of C1 holds
( dom f = (f `1 ) `1 & cod f = (f `1 ) `2 ) ) & ( for f, g being Morphism of C1 st dom g = cod f holds
[g,f] in dom the Comp of C1 ) & ( 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)] ) ) & ( for a being Object of C1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) & the carrier of C2 = Funct A,B & the carrier' of C2 = NatTrans A,B & ( for f being Morphism of C2 holds
( dom f = (f `1 ) `1 & cod f = (f `1 ) `2 ) ) & ( for f, g being Morphism of C2 st dom g = cod f holds
[g,f] in dom the Comp of C2 ) & ( 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)] ) ) & ( for a being Object of C2
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) implies C1 = C2 )
assume that
A64: the carrier of C1 = Funct A,B and
A65: the carrier' of C1 = NatTrans A,B and
A66: for f being Morphism of C1 holds
( dom f = (f `1 ) `1 & cod f = (f `1 ) `2 ) and
A67: for f, g being Morphism of C1 st dom g = cod f holds
[g,f] in dom the Comp of C1 and
A68: 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
A69: for a being Object of C1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] and
A70: the carrier of C2 = Funct A,B and
A71: the carrier' of C2 = NatTrans A,B and
A72: for f being Morphism of C2 holds
( dom f = (f `1 ) `1 & cod f = (f `1 ) `2 ) and
A73: for f, g being Morphism of C2 st dom g = cod f holds
[g,f] in dom the Comp of C2 and
A74: 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
A75: for a being Object of C2
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ; :: thesis: C1 = C2

now

thus the carrier' of C1 = the carrier' of C2 by A65, A71; :: thesis: ( the Source of C1 = the Source of C2 & the Target of C1 = the Target of C2 & the Comp of C1 = the Comp of C2 & the Id of C1 = the Id of C2 )
thus the Source of C1 = the Source of C2 :: thesis: ( the Target of C1 = the Target of C2 & the Comp of C1 = the Comp of C2 & the Id of C1 = the Id of C2 )

proof

thus the carrier' of C1 = the carrier' of C2 by A65, A71; :: according to FUNCT_2:def 8 :: thesis: for b₁ being Element of the carrier' of C1 holds the Source of C1 . b₁ = the Source of C2 . b₁
let a be Morphism of C1; :: thesis: the Source of C1 . a = the Source of C2 . a
reconsider b = a as Morphism of C2 by A65, A71;
thus the Source of C1 . a = dom a
.= (a `1 ) `1 by A66
.= dom b by A72
.= the Source of C2 . a ; :: thesis: verum

end;

thus the Target of C1 = the Target of C2 :: thesis: ( the Comp of C1 = the Comp of C2 & the Id of C1 = the Id of C2 )

proof

thus the carrier' of C1 = the carrier' of C2 by A65, A71; :: according to FUNCT_2:def 8 :: thesis: for b₁ being Element of the carrier' of C1 holds the Target of C1 . b₁ = the Target of C2 . b₁
let a be Morphism of C1; :: thesis: the Target of C1 . a = the Target of C2 . a
reconsider b = a as Morphism of C2 by A65, A71;
thus the Target of C1 . a = cod a
.= (a `1 ) `2 by A66
.= cod b by A72
.= the Target of C2 . a ; :: thesis: verum

end;

now

A76: dom the Comp of C1 c= [:the carrier' of C1,the carrier' of C1:] by RELAT_1:def 18;
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 A65, A71, RELAT_1:def 18;

now

let x be Element of [:the carrier' of C1,the carrier' of C1:]; :: thesis: ( x in S1 iff x in S2 )
A77: x = [(x `1 ),(x `2 )] by MCART_1:23;
then reconsider f1 = x `2 , g1 = x `1 as Morphism of C1 by ZFMISC_1:106;
reconsider f2 = x `2 , g2 = x `1 as Morphism of C2 by A65, A71, A77, ZFMISC_1:106;

A78: now

assume [g1,f1] in S1 ; :: thesis: [g2,f2] in S2
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
A79: ( f1 = [[F,F1],t] & g1 = [[F1,F2],t1] ) and
the Comp of C1 . [g1,f1] = [[F,F2],(t1 `*` t)] by A68;
dom g2 = (g2 `1 ) `1 by A72
.= [F1,F2] `1 by A79, MCART_1:7
.= F1 by MCART_1:7
.= [F,F1] `2 by MCART_1:7
.= (f1 `1 ) `2 by A79, MCART_1:7
.= cod f2 by A72 ;
hence [g2,f2] in S2 by A73; :: thesis: verum

end;

now

assume [g2,f2] in S2 ; :: thesis: [g1,f1] in S1
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
A80: ( f2 = [[F,F1],t] & g2 = [[F1,F2],t1] ) and
the Comp of C2 . [g2,f2] = [[F,F2],(t1 `*` t)] by A74;
dom g1 = (g1 `1 ) `1 by A66
.= [F1,F2] `1 by A80, MCART_1:7
.= F1 by MCART_1:7
.= [F,F1] `2 by MCART_1:7
.= (f2 `1 ) `2 by A80, MCART_1:7
.= cod f1 by A66 ;
hence [g1,f1] in S1 by A67; :: thesis: verum

end;

hence ( x in S1 iff x in S2 ) by A78, MCART_1:23; :: thesis: verum

end;

hence A81: dom the Comp of C1 = dom the Comp of C2 by SUBSET_1:8; :: thesis: for x being set st x in dom the Comp of C1 holds
the Comp of C1 . x = the Comp of C2 . x
let x be set ; :: thesis: ( x in dom the Comp of C1 implies the Comp of C1 . x = the Comp of C2 . x )
assume A82: x in dom the Comp of C1 ; :: thesis: the Comp of C1 . x = the Comp of C2 . x
then reconsider f = x `2 , g = x `1 as Morphism of C1 by A76, MCART_1:10;
A83: [g,f] = x by A76, A82, MCART_1:23;
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
A84: ( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] ) by A68, A82;
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
A85: ( f = [[F',F1'],t'] & g = [[F1',F2'],t1'] & the Comp of C2 . [g,f] = [[F',F2'],(t1' `*` t')] ) by A65, A71, A74, A81, A82, A83;
( [F,F1] = [F',F1'] & [F1,F2] = [F1',F2'] ) by A84, A85, ZFMISC_1:33;
then ( F = F' & F1 = F1' & F2 = F2' & t = t' & t1 = t1' ) by A84, A85, ZFMISC_1:33;
hence the Comp of C1 . x = the Comp of C2 . x by A83, A84, A85; :: thesis: verum

end;

hence the Comp of C1 = the Comp of C2 by FUNCT_1:9; :: thesis: the Id of C1 = the Id of C2
thus the Id of C1 = the Id of C2 :: thesis: verum

proof

thus the carrier of C1 = the carrier of C2 by A64, A70; :: according to FUNCT_2:def 8 :: thesis: for b₁ being Element of the carrier of C1 holds the Id of C1 . b₁ = the Id of C2 . b₁
let a be Object of C1; :: thesis: the Id of C1 . a = the Id of C2 . a
reconsider F = a as Functor of A,B by A64, CAT_2:def 3;
reconsider b = a as Object of C2 by A64, A70;
thus the Id of C1 . a = id a
.= [[F,F],(id F)] by A69
.= id b by A75
.= the Id of C2 . a ; :: thesis: verum

end;

end;

hence C1 = C2 by A64, A70; :: thesis: verum