let C1, C2 be non empty transitive AltCatStr ; :: thesis: ( C1,C2 are_opposite iff ( the carrier of C2 = the carrier of C1 & ( 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 ) ) ) ) )
A1: dom the Arrows of C1 = [: the carrier of C1, the carrier of C1:] by PARTFUN1:def 2;
A2: dom the Arrows of C2 = [: the carrier of C2, the carrier of C2:] by PARTFUN1:def 2;

hereby :: thesis: ( the carrier of C2 = the carrier of C1 & ( 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 ) ) ) implies C1,C2 are_opposite )

assume A3: C1,C2 are_opposite ; :: thesis: ( the carrier of C2 = the carrier of C1 & ( 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 ) ) ) )
hence the carrier of C2 = the carrier of C1 ; :: thesis: 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 ) )
let a, b, c be Object of C1; :: thesis: 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 ) )
let a9, b9, c9 be Object of C2; :: thesis: ( a9 = a & b9 = b & c9 = c implies ( <^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 ) ) )
assume that
A4: a9 = a and
A5: b9 = b and
A6: c9 = c ; :: thesis: ( <^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 ) )
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 ; :: thesis: ( <^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 )
A10: <^b,c^> = (~ the Arrows of C1) . (c,b) by A8, FUNCT_4:def 2
.= <^c9,b9^> by A3, A5, A6 ;
A11: the Comp of C2 . (c9,b9,a9) = ~ ( the Comp of C1 . (a,b,c)) by A3, A4, A5, A6;
assume that
A12: <^a,b^> <> {} and
A13: <^b,c^> <> {} ; :: thesis: 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
let f be Morphism of a,b; :: thesis: 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
let g be Morphism of b,c; :: thesis: for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f
<^a,c^> <> {} by A12, A13, ALTCAT_1:def 2;
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: for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f
let g9 be Morphism of c9,b9; :: thesis: ( f9 = f & g9 = g implies f9 * g9 = g * f )
assume that
A15: f9 = f and
A16: g9 = g ; :: thesis: f9 * g9 = g * f
thus f9 * g9 = (~ ( the Comp of C1 . (a,b,c))) . (f,g) by A9, A10, A11, A12, A13, A15, A16, ALTCAT_1:def 8
.= ( the Comp of C1 . (a,b,c)) . (g,f) by A14, FUNCT_4:def 2
.= g * f by A12, A13, ALTCAT_1:def 8 ; :: thesis: verum

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: C1,C2 are_opposite
thus the carrier of C2 = the carrier of C1 by A17; :: according to YELLOW18:def 3 :: thesis: ( the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) ) )

A19: now :: thesis: for x being object holds
( ( x in dom the Arrows of C2 implies ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 ) ) & ( ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 ) implies x in dom the Arrows of C2 ) )

let x be object ; :: thesis: ( ( x in dom the Arrows of C2 implies ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 ) ) & ( ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 ) implies x in dom the Arrows of C2 ) )

hereby :: thesis: ( ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 ) implies x in dom the Arrows of C2 )

assume x in dom the Arrows of C2 ; :: thesis: ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 )
then consider y, z being object such that
A20: y in the carrier of C1 and
A21: z in the carrier of C1 and
A22: [y,z] = x by A17, ZFMISC_1:def 2;
take z = z; :: thesis: ex y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 )
take y = y; :: thesis: ( x = [y,z] & [z,y] in dom the Arrows of C1 )
thus ( x = [y,z] & [z,y] in dom the Arrows of C1 ) by A1, A20, A21, A22, ZFMISC_1:def 2; :: thesis: verum

end;

given z, y being object such that A23: x = [y,z] and
A24: [z,y] in dom the Arrows of C1 ; :: thesis: x in dom the Arrows of C2
A25: z in the carrier of C1 by A24, ZFMISC_1:87;
y in the carrier of C1 by A24, ZFMISC_1:87;
hence x in dom the Arrows of C2 by A2, A17, A23, A25, ZFMISC_1:def 2; :: thesis: verum

end;

now :: thesis: for y, z being object st [y,z] in dom the Arrows of C1 holds
the Arrows of C2 . (z,y) = the Arrows of C1 . (y,z)

let y, z be object ; :: thesis: ( [y,z] in dom the Arrows of C1 implies the Arrows of C2 . (z,y) = the Arrows of C1 . (y,z) )
assume [y,z] in dom the Arrows of C1 ; :: thesis: the Arrows of C2 . (z,y) = the Arrows of C1 . (y,z)
then reconsider a = y, b = z as Object of C1 by ZFMISC_1:87;
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: verum

end;

hence the Arrows of C2 = ~ the Arrows of C1 by A19, FUNCT_4:def 2; :: thesis: for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a))
let a, b, c be Object of C1; :: thesis: for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a))
let a9, b9, c9 be Object of C2; :: thesis: ( a9 = a & b9 = b & c9 = c implies the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a)) )
assume that
A26: a9 = a and
A27: b9 = b and
A28: c9 = c ; :: thesis: the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a))
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:90;
then ( [:<^b,a^>,<^c,b^>:] <> {} implies <^c,a^> <> {} ) by ALTCAT_1:def 2;
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:90;
then ( [:<^c,b^>,<^b,a^>:] <> {} implies <^c,a^> <> {} ) by ALTCAT_1:def 2;
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 :: thesis: for x being object holds
( ( x in dom ( the Comp of C2 . (a9,b9,c9)) implies ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) ) ) & ( ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) ) implies x in dom ( the Comp of C2 . (a9,b9,c9)) ) )

let x be object ; :: thesis: ( ( x in dom ( the Comp of C2 . (a9,b9,c9)) implies ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) ) ) & ( ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) ) implies x in dom ( the Comp of C2 . (a9,b9,c9)) ) )

hereby :: thesis: ( ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) ) implies x in dom ( the Comp of C2 . (a9,b9,c9)) )

assume x in dom ( the Comp of C2 . (a9,b9,c9)) ; :: thesis: ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) )
then consider y, z being object 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: ex y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) )
take y = y; :: thesis: ( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) )
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: verum

end;

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

end;

now :: thesis: for y, z being object st [y,z] in dom ( the Comp of C1 . (c,b,a)) holds
( the Comp of C2 . (a9,b9,c9)) . (z,y) = ( the Comp of C1 . (c,b,a)) . (y,z)

let y, z be object ; :: thesis: ( [y,z] in dom ( the Comp of C1 . (c,b,a)) implies ( the Comp of C2 . (a9,b9,c9)) . (z,y) = ( the Comp of C1 . (c,b,a)) . (y,z) )
assume A41: [y,z] in dom ( the Comp of C1 . (c,b,a)) ; :: thesis: ( the Comp of C2 . (a9,b9,c9)) . (z,y) = ( the Comp of C1 . (c,b,a)) . (y,z)
then A42: y in <^b,a^> by ZFMISC_1:87;
A43: z in <^c,b^> by A41, ZFMISC_1:87;
reconsider f = y as Morphism of b,a by A41, ZFMISC_1:87;
reconsider g = z as Morphism of c,b by A41, ZFMISC_1:87;
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 8
.= f * g by A18, A26, A27, A28, A42, A43
.= ( the Comp of C1 . (c,b,a)) . (y,z) by A42, A43, ALTCAT_1:def 8 ; :: thesis: verum

end;

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