let A, B be non empty AltCatStr ; :: thesis: ( A,B are_opposite implies for a, b being object of A
for a9, b9 being object of B st a9 = a & b9 = b holds
<^a,b^> = <^b9,a9^> )
assume that
the carrier of B = the carrier of A and
A1: the Arrows of B = ~ the Arrows of A ; :: according to YELLOW18:def 3 :: thesis: ( ex a, b, c being object of A ex a9, b9, c9 being object of B st
( a9 = a & b9 = b & c9 = c & not the Comp of B . (a9,b9,c9) = ~ ( the Comp of A . (c,b,a)) ) or for a, b being object of A
for a9, b9 being object of B st a9 = a & b9 = b holds
<^a,b^> = <^b9,a9^> )
assume for a, b, c being object of A
for a9, b9, c9 being object of B st a9 = a & b9 = b & c9 = c holds
the Comp of B . (a9,b9,c9) = ~ ( the Comp of A . (c,b,a)) ; :: thesis: for a, b being object of A
for a9, b9 being object of B st a9 = a & b9 = b holds
<^a,b^> = <^b9,a9^>
let a, b be object of A; :: thesis: for a9, b9 being object of B st a9 = a & b9 = b holds
<^a,b^> = <^b9,a9^>
let a9, b9 be object of B; :: thesis: ( a9 = a & b9 = b implies <^a,b^> = <^b9,a9^> )
thus ( a9 = a & b9 = b implies <^a,b^> = <^b9,a9^> ) by A1, ALTCAT_2:6; :: thesis: verum