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)

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)

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

then A75:
the Arrows of C1 = the Arrows of C2
by A66, A69, ALTCAT_1:6;
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 A69, A74, Def10;

reconsider f = i as strict covariant Functor of A,B by A66, A73, Def10;

end;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 A69, A74, Def10;

reconsider f = i as strict covariant Functor of A,B by A66, A73, Def10;

now :: thesis: for x being object holds

( x in the Arrows of C1 . (i,j) iff x in the Arrows of C2 . (i,j) )

hence
the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
by TARSKI:2; :: thesis: verum( 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;( 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

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

hence
C1 = C2
by A66, A69, A75, ALTCAT_1:8; :: thesis: verum
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 A66, A78, Def10;

reconsider g = j as strict covariant Functor of A,B by A66, A77, Def10;

reconsider f = i as strict covariant Functor of A,B by A66, A76, Def10;

end;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 A66, A78, Def10;

reconsider g = j as strict covariant Functor of A,B by A66, A77, Def10;

reconsider f = i as strict covariant Functor of A,B by A66, A76, Def10;

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) <> {} ) )
;

end;

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

end;proof
end;

per cases
( the Arrows of C1 . (i,j) = {} or the Arrows of C1 . (j,k) = {} )
by A79;

end;

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 A66, A69, A72, A80, ALTCAT_1:6;

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 A82, A83, PBOOLE:def 15;

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 A66, A69, A75, A85, A86, PBOOLE:def 15;

hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A81, A84; :: thesis: verum

end;reconsider i9 = i, j9 = j, k9 = k as Element of T by A66, A69, A76, A77, A78;

the Arrows of C2 . (i,j) = {} by A66, A69, A72, A80, ALTCAT_1:6;

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 A82, A83, PBOOLE:def 15;

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 A66, A69, A75, A85, A86, PBOOLE:def 15;

hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A81, A84; :: thesis: verum

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 A66, A69, A72, A87, ALTCAT_1:6;

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 A89, A90, PBOOLE:def 15;

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 A66, A69, A75, A92, A93, PBOOLE:def 15;

hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A88, A91; :: thesis: verum

end;reconsider i9 = i, j9 = j, k9 = k as Element of T by A66, A69, A76, A77, A78;

the Arrows of C2 . (j,k) = {} by A66, A69, A72, A87, ALTCAT_1:6;

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 A89, A90, PBOOLE:def 15;

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 A66, A69, A75, A92, A93, PBOOLE:def 15;

hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A88, A91; :: thesis: verum

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)

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 A96, A97, PBOOLE:def 15;

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 A66, A69, A75, A98, A99, PBOOLE:def 15;

A100: the Arrows of C2 . (j,k) <> {} by A66, A69, A72, A95, ALTCAT_1:6;

A101: the Arrows of C2 . (i,j) <> {} by A66, A69, A72, A94, ALTCAT_1:6;

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)

end;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 A96, A97, PBOOLE:def 15;

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 A66, A69, A75, A98, A99, PBOOLE:def 15;

A100: the Arrows of C2 . (j,k) <> {} by A66, A69, A72, A95, ALTCAT_1:6;

A101: the Arrows of C2 . (i,j) <> {} by A66, A69, A72, A94, ALTCAT_1:6;

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

hence
the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
by BINOP_1:2; :: thesis: verum
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 A70, A100;

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 A70, A101;

( 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 A68, A71, A102, A103;

hence t1 . (a,b) = t2 . (a,b) ; :: thesis: verum

end;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 A70, A100;

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 A70, A101;

( 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 A68, A71, A102, A103;

hence t1 . (a,b) = t2 . (a,b) ; :: thesis: verum