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 4;
A8:
dom the
Comp of
C2 = [:the carrier of C2,the carrier of C2,the carrier of C2:]
by PARTFUN1:def 4;
now let x be
set ;
( 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
set 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:72;
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:9;
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