let C1, C2 be non empty transitive strict AltCatStr ; :: thesis: ( the carrier of C1 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of C1 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of C1 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) & the carrier of C2 = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of C2 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of C2 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) implies C1 = C2 )

assume that
A66: the carrier of C1 = Funct (A,B) and
A67: for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of C1 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) and
A68: for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of C1 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) and
A69: the carrier of C2 = Funct (A,B) and
A70: for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of C2 . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) and
A71: for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of C2 . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ; :: thesis: C1 = C2
set R = the carrier of C1;
set T = the carrier of C2;
set N = the Arrows of C1;
set M = the Arrows of C2;
set O = the Comp of C1;
set P = the Comp of C2;
A72: for i, j being object st i in the carrier of C1 & j in the carrier of C2 holds
the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
proof
let i, j be object ; :: thesis: ( i in the carrier of C1 & j in the carrier of C2 implies the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) )
assume that
A73: i in the carrier of C1 and
A74: j in the carrier of C2 ; :: thesis: the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
reconsider g = j as strict covariant Functor of A,B by ;
reconsider f = i as strict covariant Functor of A,B by ;
now :: thesis: for x being object holds
( x in the Arrows of C1 . (i,j) iff x in the Arrows of C2 . (i,j) )
let x be object ; :: thesis: ( x in the Arrows of C1 . (i,j) iff x in the Arrows of C2 . (i,j) )
( x in the Arrows of C1 . (i,j) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) by A67;
hence ( x in the Arrows of C1 . (i,j) iff x in the Arrows of C2 . (i,j) ) by A70; :: thesis: verum
end;
hence the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) by TARSKI:2; :: thesis: verum
end;
then A75: the Arrows of C1 = the Arrows of C2 by ;
for i, j, k being object st i in the carrier of C1 & j in the carrier of C1 & k in the carrier of C1 holds
the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
proof
let i, j, k be object ; :: thesis: ( i in the carrier of C1 & j in the carrier of C1 & k in the carrier of C1 implies the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) )
assume that
A76: i in the carrier of C1 and
A77: j in the carrier of C1 and
A78: k in the carrier of C1 ; :: thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
reconsider h = k as strict covariant Functor of A,B by ;
reconsider g = j as strict covariant Functor of A,B by ;
reconsider f = i as strict covariant Functor of A,B by ;
per cases ( the Arrows of C1 . (i,j) = {} or the Arrows of C1 . (j,k) = {} or ( the Arrows of C1 . (i,j) <> {} & the Arrows of C1 . (j,k) <> {} ) ) ;
suppose A79: ( the Arrows of C1 . (i,j) = {} or the Arrows of C1 . (j,k) = {} ) ; :: thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
thus the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) :: thesis: verum
proof
per cases ( the Arrows of C1 . (i,j) = {} or the Arrows of C1 . (j,k) = {} ) by A79;
suppose A80: the Arrows of C1 . (i,j) = {} ; :: thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
reconsider T = the carrier of C2 as non empty set ;
reconsider i9 = i, j9 = j, k9 = k as Element of T by A66, A69, A76, A77, A78;
the Arrows of C2 . (i,j) = {} by ;
then A81: [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] = {} by ZFMISC_1:90;
A82: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def 4 ;
A83: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def 3 ;
the Comp of C2 . [i9,j9,k9] = the Comp of C2 . (i9,j9,k9) by MULTOP_1:def 1;
then A84: the Comp of C2 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by ;
A85: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def 4 ;
A86: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def 3 ;
the Comp of C1 . [i9,j9,k9] = the Comp of C1 . (i9,j9,k9) by MULTOP_1:def 1;
then the Comp of C1 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by ;
hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by ; :: thesis: verum
end;
suppose A87: the Arrows of C1 . (j,k) = {} ; :: thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
reconsider T = the carrier of C2 as non empty set ;
reconsider i9 = i, j9 = j, k9 = k as Element of T by A66, A69, A76, A77, A78;
the Arrows of C2 . (j,k) = {} by ;
then A88: [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] = {} by ZFMISC_1:90;
A89: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def 4 ;
A90: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def 3 ;
the Comp of C2 . [i9,j9,k9] = the Comp of C2 . (i9,j9,k9) by MULTOP_1:def 1;
then A91: the Comp of C2 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by ;
A92: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def 4 ;
A93: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def 3 ;
the Comp of C1 . [i9,j9,k9] = the Comp of C1 . (i9,j9,k9) by MULTOP_1:def 1;
then the Comp of C1 . (i9,j9,k9) is Function of [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):],( the Arrows of C2 . (i9,k9)) by ;
hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by ; :: thesis: verum
end;
end;
end;
end;
suppose that A94: the Arrows of C1 . (i,j) <> {} and
A95: the Arrows of C1 . (j,k) <> {} ; :: thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
reconsider T = the carrier of C2 as non empty set ;
reconsider i9 = i, j9 = j, k9 = k as Element of T by A66, A69, A76, A77, A78;
A96: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def 4 ;
A97: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def 3 ;
the Comp of C2 . [i9,j9,k9] = the Comp of C2 . (i9,j9,k9) by MULTOP_1:def 1;
then reconsider t2 = the Comp of C2 . (i,j,k) as Function of [:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):],( the Arrows of C2 . (i,k)) by ;
A98: {| the Arrows of C2, the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2, the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= [:( the Arrows of C2 . (j9,k9)),( the Arrows of C2 . (i9,j9)):] by ALTCAT_1:def 4 ;
A99: {| the Arrows of C2|} . [i9,j9,k9] = {| the Arrows of C2|} . (i9,j9,k9) by MULTOP_1:def 1
.= the Arrows of C2 . (i9,k9) by ALTCAT_1:def 3 ;
the Comp of C1 . [i9,j9,k9] = the Comp of C1 . (i9,j9,k9) by MULTOP_1:def 1;
then reconsider t1 = the Comp of C1 . (i,j,k) as Function of [:( the Arrows of C2 . (j,k)),( the Arrows of C2 . (i,j)):],( the Arrows of C2 . (i,k)) by ;
A100: the Arrows of C2 . (j,k) <> {} by ;
A101: the Arrows of C2 . (i,j) <> {} by ;
for a being Element of the Arrows of C2 . (j,k)
for b being Element of the Arrows of C2 . (i,j) holds t1 . (a,b) = t2 . (a,b)
proof
let a be Element of the Arrows of C2 . (j,k); :: thesis: for b being Element of the Arrows of C2 . (i,j) holds t1 . (a,b) = t2 . (a,b)
let b be Element of the Arrows of C2 . (i,j); :: thesis: t1 . (a,b) = t2 . (a,b)
a in the Arrows of C2 . (j,k) by A100;
then A102: g is_naturally_transformable_to h by A70;
reconsider a = a as natural_transformation of g,h by ;
b in the Arrows of C2 . (i,j) by A101;
then A103: f is_naturally_transformable_to g by A70;
reconsider b = b as natural_transformation of f,g by ;
( ex t19 being Function st
( t19 = the Comp of C1 . (f,g,h) & t19 . (a,b) = a `*` b ) & ex t29 being Function st
( t29 = the Comp of C2 . (f,g,h) & t29 . (a,b) = a `*` b ) ) by ;
hence t1 . (a,b) = t2 . (a,b) ; :: thesis: verum
end;
hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by BINOP_1:2; :: thesis: verum
end;
end;
end;
hence C1 = C2 by ; :: thesis: verum