let C, C1, C2 be non empty AltCatStr ; ( C,C1 are_opposite implies ( C,C2 are_opposite iff AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) ) )
assume that
A1:
the carrier of C1 = the carrier of C
and
A2:
the Arrows of C1 = ~ the Arrows of C
and
A3:
for a, b, c being Object of C
for a9, b9, c9 being Object of C1 st a9 = a & b9 = b & c9 = c holds
the Comp of C1 . (a9,b9,c9) = ~ ( the Comp of C . (c,b,a))
; YELLOW18:def 3 ( C,C2 are_opposite iff AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) )
thus
( C,C2 are_opposite implies AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) )
( AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) implies C,C2 are_opposite )proof
assume that A4:
the
carrier of
C2 = the
carrier of
C
and A5:
the
Arrows of
C2 = ~ the
Arrows of
C
and A6:
for
a,
b,
c being
Object of
C 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 C . (c,b,a))
;
YELLOW18:def 3 AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
A7:
dom the
Comp of
C1 = [: the carrier of C1, the carrier of C1, the carrier of C1:]
by PARTFUN1:def 2;
A8:
dom the
Comp of
C2 = [: the carrier of C2, the carrier of C2, the carrier of C2:]
by PARTFUN1:def 2;
now for x being object st x in [: the carrier of C, the carrier of C, the carrier of C:] holds
the Comp of C1 . x = the Comp of C2 . xlet x be
object ;
( x in [: the carrier of C, the carrier of C, the carrier of C:] implies the Comp of C1 . x = the Comp of C2 . x )assume
x in [: the carrier of C, the carrier of C, the carrier of C:]
;
the Comp of C1 . x = the Comp of C2 . xthen consider a,
b,
c being
object such that A9:
a in the
carrier of
C
and A10:
b in the
carrier of
C
and A11:
c in the
carrier of
C
and A12:
x = [a,b,c]
by MCART_1:68;
reconsider a =
a,
b =
b,
c =
c as
Object of
C by A9, A10, A11;
reconsider a1 =
a,
b1 =
b,
c1 =
c as
Object of
C1 by A1;
reconsider a2 =
a,
b2 =
b,
c2 =
c as
Object of
C2 by A4;
A13:
the
Comp of
C1 . (
a1,
b1,
c1)
= ~ ( the Comp of C . (c,b,a))
by A3;
the
Comp of
C2 . (
a2,
b2,
c2)
= ~ ( the Comp of C . (c,b,a))
by A6;
hence the
Comp of
C1 . x =
the
Comp of
C2 . (
a2,
b2,
c2)
by A12, A13, MULTOP_1:def 1
.=
the
Comp of
C2 . x
by A12, MULTOP_1:def 1
;
verum end;
hence
AltCatStr(# the
carrier of
C1, the
Arrows of
C1, the
Comp of
C1 #)
= AltCatStr(# the
carrier of
C2, the
Arrows of
C2, the
Comp of
C2 #)
by A1, A2, A4, A5, A7, A8, FUNCT_1:2;
verum
end;
assume A14:
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #)
; C,C2 are_opposite
hence
( the carrier of C2 = the carrier of C & the Arrows of C2 = ~ the Arrows of C )
by A1, A2; YELLOW18:def 3 for a, b, c being Object of C
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 C . (c,b,a))
let a, b, c be Object of C; 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 C . (c,b,a))
let a9, b9, c9 be Object of C2; ( a9 = a & b9 = b & c9 = c implies the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C . (c,b,a)) )
thus
( a9 = a & b9 = b & c9 = c implies the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C . (c,b,a)) )
by A3, A14; verum