let C, C1, C2 be non empty AltCatStr ; :: thesis: ( 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 a', b', c' being object of C1 st a' = a & b' = b & c' = c holds
the Comp of C1 . a',b',c' = ~ (the Comp of C . c,b,a)
; :: according to YELLOW18:def 3 :: thesis: ( 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 #) )
:: thesis: ( 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
a',
b',
c' being
object of
C2 st
a' = a &
b' = b &
c' = c holds
the
Comp of
C2 . a',
b',
c' = ~ (the Comp of C . c,b,a)
;
:: according to YELLOW18:def 3 :: thesis: 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 ;
:: thesis: ( 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:]
;
:: thesis: 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 &
b in the
carrier of
C &
c in the
carrier of
C &
x = [a,b,c] )
by MCART_1:72;
reconsider a =
a,
b =
b,
c =
c as
object of
C by A9;
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;
( the
Comp of
C1 . a1,
b1,
c1 = ~ (the Comp of C . c,b,a) & the
Comp of
C2 . a2,
b2,
c2 = ~ (the Comp of C . c,b,a) )
by A3, A6;
hence the
Comp of
C1 . x =
the
Comp of
C2 . a2,
b2,
c2
by A9, MULTOP_1:def 1
.=
the
Comp of
C2 . x
by A9, MULTOP_1:def 1
;
:: thesis: 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;
:: thesis: verum
end;
assume A10:
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 #)
; :: thesis: C,C2 are_opposite
hence
( the carrier of C2 = the carrier of C & the Arrows of C2 = ~ the Arrows of C )
by A1, A2; :: according to YELLOW18:def 3 :: thesis: for a, b, c being object of C
for a', b', c' being object of C2 st a' = a & b' = b & c' = c holds
the Comp of C2 . a',b',c' = ~ (the Comp of C . c,b,a)
let a, b, c be object of C; :: thesis: for a', b', c' being object of C2 st a' = a & b' = b & c' = c holds
the Comp of C2 . a',b',c' = ~ (the Comp of C . c,b,a)
let a', b', c' be object of C2; :: thesis: ( a' = a & b' = b & c' = c implies the Comp of C2 . a',b',c' = ~ (the Comp of C . c,b,a) )
thus
( a' = a & b' = b & c' = c implies the Comp of C2 . a',b',c' = ~ (the Comp of C . c,b,a) )
by A3, A10; :: thesis: verum