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

hereby :: thesis:

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 a', b', c' be object of C2; :: thesis:
assume that
A4: a' = a and
A5: b' = b and
A6: c' = 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
.= <^b',a'^> by A3, A4, A5, Def3 ; :: thesis:
A10: <^b,c^> = (~ the Arrows of C1) . c,b by A8, FUNCT_4:def 2
.= <^c',b'^> by A3, A5, A6, Def3 ;
A11: the Comp of C2 . c',b',a' = ~ (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 f' be Morphism of b',a'; :: thesis:
let g' be Morphism of c',b'; :: thesis:
assume that
A15: f' = f and
A16: g' = g ; :: thesis:
thus f' * g' = (~ (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 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 A17; :: according to YELLOW18:def 3 :: thesis:

A19: 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
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;

given z, y being set such that A23: x = [y,z] and
A24: [z,y] in dom the Arrows of C1 ; :: thesis:
A25: z in the carrier of C1 by A1, A24, ZFMISC_1:106;
y in the carrier of C1 by A1, A24, ZFMISC_1:106;
hence x in dom the Arrows of C2 by A2, A17, A23, A25, 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 A17;
thus the Arrows of C2 . z,y = <^b',a'^>
.= <^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 a', b', c' be object of C2; :: thesis:
assume that
A26: a' = a and
A27: b' = b and
A28: c' = c ; :: thesis:
A29: <^a',b'^> = <^b,a^> by A18, A26, A27;
A30: <^b',c'^> = <^c,b^> by A18, A27, A28;
A31: <^a',c'^> = <^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 . a',b',c') = [:(the Arrows of C2 . b',c'),(the Arrows of C2 . a',b'):] by A29, A30, A31, FUNCT_2:def 1;

A34: 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
A35: y in <^b',c'^> and
A36: z in <^a',b'^> 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;

given z, y being set such that A38: x = [y,z] and
A39: [z,y] in dom (the Comp of C1 . c,b,a) ; :: thesis:
A40: z in <^b,a^> by A39, ZFMISC_1:106;
y in <^c,b^> by A39, ZFMISC_1:106;
hence x in dom (the Comp of C2 . a',b',c') by A29, A30, A33, A38, A40, ZFMISC_1:def 2; :: thesis:

end;

now

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 f' = y as Morphism of a',b' by A18, A26, A27, A42;
reconsider g' = z as Morphism of b',c' by A18, A27, A28, A43;
thus (the Comp of C2 . a',b',c') . z,y = g' * f' 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 . a',b',c' = ~ (the Comp of C1 . c,b,a) by A34, FUNCT_4:def 2; :: thesis: