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 :: thesis: for a, b, c being Element of C
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 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 2;
H₂(a,b,c,f,g) = f9 * g9 by A2, A4, ALTCAT_1:def 8;
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 :: thesis: for a, b, c being Object of C
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 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 8 ; :: thesis: verum

end;

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