let C1, C2 be non empty transitive AltCatStr ; :: thesis:
A1: ( dom the Arrows of C1 = [:the carrier of C1,the carrier of C1:] & dom the Arrows of C2 = [:the carrier of C2,the carrier of C2:] ) by PARTFUN1:def 4;

hereby :: thesis:

assume A2: C1,C2 are_opposite ; :: thesis:
hence the carrier of C2 = the carrier of C1 by Def3; :: thesis:
let a, b, c be object of C1; :: thesis:
let a', b', c' be object of C2; :: thesis:
assume A3: ( a' = a & b' = b & c' = c ) ; :: thesis:
A4: ( [a,b] in dom the Arrows of C1 & [b,c] in dom the Arrows of C1 & [a,c] in dom the Arrows of C1 ) by A1, ZFMISC_1:def 2;
hence A5: <^a,b^> = (~ the Arrows of C1) . b,a by FUNCT_4:def 2
.= <^b',a'^> by A2, A3, Def3 ;
:: thesis:
A6: <^b,c^> = (~ the Arrows of C1) . c,b by A4, FUNCT_4:def 2
.= <^c',b'^> by A2, A3, Def3 ;
A7: the Comp of C2 . c',b',a' = ~ (the Comp of C1 . a,b,c) by A2, A3, Def3;
assume A8: ( <^a,b^> <> {} & <^b,c^> <> {} ) ; :: thesis:
let f be Morphism of a,b; :: thesis:
let g be Morphism of b,c; :: thesis:
<^a,c^> <> {} by A8, ALTCAT_1:def 4;
then dom (the Comp of C1 . a,b,c) = [:(the Arrows of C1 . b,c),(the Arrows of C1 . a,b):] by FUNCT_2:def 1;
then A9: [g,f] in dom (the Comp of C1 . a,b,c) by A8, ZFMISC_1:def 2;
let f' be Morphism of b',a'; :: thesis:
let g' be Morphism of c',b'; :: thesis:
assume ( f' = f & g' = g ) ; :: thesis:
hence f' * g' = (~ (the Comp of C1 . a,b,c)) . f,g by A5, A6, A7, A8, ALTCAT_1:def 10
.= (the Comp of C1 . a,b,c) . g,f by A9, FUNCT_4:def 2
.= g * f by A8, ALTCAT_1:def 10 ;
:: thesis:

end;

assume that
A10: the carrier of C2 = the carrier of C1 and
A11: for a, b, c being object of C1
for a', b', c' being object of C2 st a' = a & b' = b & c' = c holds
( <^a,b^> = <^b',a'^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = f & g' = g holds
f' * g' = g * f ) ) ; :: thesis:
thus the carrier of C2 = the carrier of C1 by A10; :: according to YELLOW18:def 3 :: thesis:

A12: now

let x be set ; :: thesis:

hereby :: thesis:

assume x in dom the Arrows of C2 ; :: thesis:
then consider y, z being set such that
A13: ( y in the carrier of C1 & z in the carrier of C1 & [y,z] = x ) by A1, A10, ZFMISC_1:def 2;
take z = z; :: thesis:
take y = y; :: thesis:
thus ( x = [y,z] & [z,y] in dom the Arrows of C1 ) by A1, A13, ZFMISC_1:def 2; :: thesis:

end;

given z, y being set such that A14: ( x = [y,z] & [z,y] in dom the Arrows of C1 ) ; :: thesis:
( z in the carrier of C1 & y in the carrier of C1 ) by A1, A14, ZFMISC_1:106;
hence x in dom the Arrows of C2 by A1, A10, A14, ZFMISC_1:def 2; :: thesis:

end;

now

let y, z be set ; :: thesis:
assume [y,z] in dom the Arrows of C1 ; :: thesis:
then reconsider a = y, b = z as object of C1 by A1, ZFMISC_1:106;
reconsider a' = a, b' = b as object of C2 by A10;
thus the Arrows of C2 . z,y = <^b',a'^>
.= <^a,b^> by A11
.= the Arrows of C1 . y,z ; :: thesis:

end;

hence the Arrows of C2 = ~ the Arrows of C1 by A12, FUNCT_4:def 2; :: thesis:
let a, b, c be object of C1; :: thesis:
let a', b', c' be object of C2; :: thesis:
assume A15: ( a' = a & b' = b & c' = c ) ; :: thesis:
A16: ( <^a',b'^> = <^b,a^> & <^b',c'^> = <^c,b^> & <^a',c'^> = <^c,a^> ) by A11, A15;
( [:<^b,a^>,<^c,b^>:] <> {} implies ( <^b,a^> <> {} & <^c,b^> <> {} ) ) by ZFMISC_1:113;
then ( [:<^b,a^>,<^c,b^>:] <> {} implies <^c,a^> <> {} ) by ALTCAT_1:def 4;
then A17: dom (the Comp of C1 . c,b,a) = [:(the Arrows of C1 . b,a),(the Arrows of C1 . c,b):] by FUNCT_2:def 1;
( [:<^c,b^>,<^b,a^>:] <> {} implies ( <^b,a^> <> {} & <^c,b^> <> {} ) ) by ZFMISC_1:113;
then ( [:<^c,b^>,<^b,a^>:] <> {} implies <^c,a^> <> {} ) by ALTCAT_1:def 4;
then A18: dom (the Comp of C2 . a',b',c') = [:(the Arrows of C2 . b',c'),(the Arrows of C2 . a',b'):] by A16, FUNCT_2:def 1;

A19: now

let x be set ; :: thesis:

hereby :: thesis:

assume x in dom (the Comp of C2 . a',b',c') ; :: thesis:
then consider y, z being set such that
A20: ( y in <^b',c'^> & z in <^a',b'^> & [y,z] = x ) by ZFMISC_1:def 2;
take z = z; :: thesis:
take y = y; :: thesis:
thus ( x = [y,z] & [z,y] in dom (the Comp of C1 . c,b,a) ) by A16, A17, A20, ZFMISC_1:def 2; :: thesis:

end;

given z, y being set such that A21: ( x = [y,z] & [z,y] in dom (the Comp of C1 . c,b,a) ) ; :: thesis:
( z in <^b,a^> & y in <^c,b^> ) by A21, ZFMISC_1:106;
hence x in dom (the Comp of C2 . a',b',c') by A16, A18, A21, ZFMISC_1:def 2; :: thesis:

end;

now

let y, z be set ; :: thesis:
assume A22: [y,z] in dom (the Comp of C1 . c,b,a) ; :: thesis:
then A23: ( y in <^b,a^> & z in <^c,b^> ) by ZFMISC_1:106;
reconsider f = y as Morphism of b,a by A22, ZFMISC_1:106;
reconsider g = z as Morphism of c,b by A22, ZFMISC_1:106;
reconsider f' = y as Morphism of a',b' by A11, A15, A23;
reconsider g' = z as Morphism of b',c' by A11, A15, A23;
thus (the Comp of C2 . a',b',c') . z,y = g' * f' by A16, A23, ALTCAT_1:def 10
.= f * g by A11, A15, A23
.= (the Comp of C1 . c,b,a) . y,z by A23, ALTCAT_1:def 10 ; :: thesis:

end;

hence the Comp of C2 . a',b',c' = ~ (the Comp of C1 . c,b,a) by A19, FUNCT_4:def 2; :: thesis: