let A, B be non empty AltCatStr ; :: thesis: ( A,B are_opposite implies for a, b being object of A
for a', b' being object of B st a' = a & b' = b holds
<^a,b^> = <^b',a'^> )
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 a', b', c' being object of B st
( a' = a & b' = b & c' = c & not the Comp of B . a',b',c' = ~ (the Comp of A . c,b,a) ) or for a, b being object of A
for a', b' being object of B st a' = a & b' = b holds
<^a,b^> = <^b',a'^> )
assume for a, b, c being object of A
for a', b', c' being object of B st a' = a & b' = b & c' = c holds
the Comp of B . a',b',c' = ~ (the Comp of A . c,b,a) ; :: thesis: for a, b being object of A
for a', b' being object of B st a' = a & b' = b holds
<^a,b^> = <^b',a'^>
let a, b be object of A; :: thesis: for a', b' being object of B st a' = a & b' = b holds
<^a,b^> = <^b',a'^>
let a', b' be object of B; :: thesis: ( a' = a & b' = b implies <^a,b^> = <^b',a'^> )
thus ( a' = a & b' = b implies <^a,b^> = <^b',a'^> ) by A1, ALTCAT_2:6; :: thesis: verum