let C be non empty transitive AltCatStr ; :: thesis: ex C9 being non empty transitive strict AltCatStr st C,C9 are_opposite
deffunc H₁( set , set ) -> set = the Arrows of C . $2,$1;
deffunc H₂( set , set , set , set , set ) -> set = (the Comp of C . $3,$2,$1) . $4,$5;

A1: now

let a, b, c be Element of C; :: thesis: for f, g being set st f in H₁(a,b) & g in H₁(b,c) holds
H₂(a,b,c,f,g) in H₁(a,c)
let f, g be set ; :: thesis: ( f in H₁(a,b) & g in H₁(b,c) implies H₂(a,b,c,f,g) in H₁(a,c) )
reconsider a9 = a, b9 = b, c9 = c as object of C ;
assume A2: f in H₁(a,b) ; :: thesis: ( g in H₁(b,c) implies H₂(a,b,c,f,g) in H₁(a,c) )
then A3: f in <^b9,a9^> ;
reconsider f9 = f as Morphism of b9,a9 by A2;
assume A4: g in H₁(b,c) ; :: thesis: H₂(a,b,c,f,g) in H₁(a,c)
then A5: g in <^c9,b9^> ;
reconsider g9 = g as Morphism of c9,b9 by A4;
A6: <^c9,a9^> <> {} by A3, A5, ALTCAT_1:def 4;
H₂(a,b,c,f,g) = f9 * g9 by A2, A4, ALTCAT_1:def 10;
hence H₂(a,b,c,f,g) in H₁(a,c) by A6; :: thesis: verum

end;

ex C1 being non empty transitive strict AltCatStr st
( the carrier of C1 = the carrier of C & ( for a, b being object of C1 holds <^a,b^> = H₁(a,b) ) & ( for a, b, c being object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H₂(a,b,c,f,g) ) ) from YELLOW18:sch 1(A1);
then consider C1 being non empty transitive strict AltCatStr such that
A7: the carrier of C1 = the carrier of C and
A8: for a, b being object of C1 holds <^a,b^> = the Arrows of C . b,a and
A9: for a, b, c being object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (the Comp of C . c,b,a) . f,g ;
take C1 ; :: thesis: C,C1 are_opposite

now

let a, b, c be object of C; :: thesis: for a9, b9, c9 being object of C1 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 C1; :: 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
A10: a9 = a and
A11: b9 = b and
A12: 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 ) )
thus A13: <^a,b^> = <^b9,a9^> by A8, A10, A11; :: 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 )
A14: <^b,c^> = <^c9,b9^> by A8, A11, A12;
assume that
A15: <^a,b^> <> {} and
A16: <^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
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
A17: f9 = f and
A18: g9 = g ; :: thesis: f9 * g9 = g * f
thus f9 * g9 = (the Comp of C . a,b,c) . g,f by A9, A10, A11, A12, A13, A14, A15, A16, A17, A18
.= g * f by A15, A16, ALTCAT_1:def 10 ; :: thesis: verum

end;

hence C,C1 are_opposite by A7, Th9; :: thesis: verum