assume A3: 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 a9, b9, c9 be object of C2; :: thesis:
assume that
A4: a9 = a and
A5: b9 = b and
A6: c9 = c ; :: thesis:
A7: [a,b] in dom the Arrows of C1 by A1, ZFMISC_1:def 2;
A8: [b,c] in dom the Arrows of C1 by A1, ZFMISC_1:def 2;
thus A9: <^a,b^> = (~ the Arrows of C1) . b,a by A7, FUNCT_4:def 2
.= <^b9,a9^> by A3, A4, A5, Def3 ; :: thesis:
A10: <^b,c^> = (~ the Arrows of C1) . c,b by A8, FUNCT_4:def 2
.= <^c9,b9^> by A3, A5, A6, Def3 ;
A11: the Comp of C2 . c9,b9,a9 = ~ (the Comp of C1 . a,b,c) by A3, A4, A5, A6, Def3;
assume that
A12: <^a,b^> <> {} and
A13: <^b,c^> <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
let g be Morphism of b,c; :: thesis:
<^a,c^> <> {} by A12, A13, 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 A14: [g,f] in dom (the Comp of C1 . a,b,c) by A12, A13, ZFMISC_1:def 2;
let f9 be Morphism of b9,a9; :: thesis:
let g9 be Morphism of c9,b9; :: thesis:
assume that
A15: f9 = f and
A16: g9 = g ; :: thesis:
thus f9 * g9 = (~ (the Comp of C1 . a,b,c)) . f,g by A9, A10, A11, A12, A13, A15, A16, ALTCAT_1:def 10
.= (the Comp of C1 . a,b,c) . g,f by A14, FUNCT_4:def 2
.= g * f by A12, A13, ALTCAT_1:def 10 ; :: thesis:

end;

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

A19: now

let x be set ; :: thesis:

assume x in dom the Arrows of C2 ; :: thesis:
then consider y, z being set such that
A20: y in the carrier of C1 and
A21: z in the carrier of C1 and
A22: [y,z] = x by A2, A17, 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, A20, A21, A22, ZFMISC_1:def 2; :: thesis:

end;

end;

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 a9 = a, b9 = b as object of C2 by A17;
thus the Arrows of C2 . z,y = <^b9,a9^>
.= <^a,b^> by A18
.= the Arrows of C1 . y,z ; :: thesis:

end;

hence the Arrows of C2 = ~ the Arrows of C1 by A19, FUNCT_4:def 2; :: thesis:
let a, b, c be object of C1; :: thesis:
let a9, b9, c9 be object of C2; :: thesis:
assume that
A26: a9 = a and
A27: b9 = b and
A28: c9 = c ; :: thesis:
A29: <^a9,b9^> = <^b,a^> by A18, A26, A27;
A30: <^b9,c9^> = <^c,b^> by A18, A27, A28;
A31: <^a9,c9^> = <^c,a^> by A18, A26, A28;
( [:<^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 A32: 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 A33: dom (the Comp of C2 . a9,b9,c9) = [:(the Arrows of C2 . b9,c9),(the Arrows of C2 . a9,b9):] by A29, A30, A31, FUNCT_2:def 1;

A34: now

let x be set ; :: thesis:

assume x in dom (the Comp of C2 . a9,b9,c9) ; :: thesis:
then consider y, z being set such that
A35: y in <^b9,c9^> and
A36: z in <^a9,b9^> and
A37: [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 A29, A30, A32, A35, A36, A37, ZFMISC_1:def 2; :: thesis:

end;

end;

let y, z be set ; :: thesis:
assume A41: [y,z] in dom (the Comp of C1 . c,b,a) ; :: thesis:
then A42: y in <^b,a^> by ZFMISC_1:106;
A43: z in <^c,b^> by A41, ZFMISC_1:106;
reconsider f = y as Morphism of b,a by A41, ZFMISC_1:106;
reconsider g = z as Morphism of c,b by A41, ZFMISC_1:106;
reconsider f9 = y as Morphism of a9,b9 by A18, A26, A27, A42;
reconsider g9 = z as Morphism of b9,c9 by A18, A27, A28, A43;
thus (the Comp of C2 . a9,b9,c9) . z,y = g9 * f9 by A29, A30, A42, A43, ALTCAT_1:def 10
.= f * g by A18, A26, A27, A28, A42, A43
.= (the Comp of C1 . c,b,a) . y,z by A42, A43, ALTCAT_1:def 10 ; :: thesis:

end;

hence the Comp of C2 . a9,b9,c9 = ~ (the Comp of C1 . c,b,a) by A34, FUNCT_4:def 2; :: thesis: