let C1, C2 be non empty transitive AltCatStr ; ( C1,C2 are_opposite iff ( the carrier of C2 = the carrier of C1 & ( for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) ) ) ) )
A1:
dom the Arrows of C1 = [: the carrier of C1, the carrier of C1:]
by PARTFUN1:def 2;
A2:
dom the Arrows of C2 = [: the carrier of C2, the carrier of C2:]
by PARTFUN1:def 2;
hereby ( the carrier of C2 = the carrier of C1 & ( for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) ) ) implies C1,C2 are_opposite )
assume A3:
C1,
C2 are_opposite
;
( the carrier of C2 = the carrier of C1 & ( for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) ) ) )hence
the
carrier of
C2 = the
carrier of
C1
;
for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) )let a,
b,
c be
Object of
C1;
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) )let a9,
b9,
c9 be
Object of
C2;
( a9 = a & b9 = b & c9 = c implies ( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) ) )assume that A4:
a9 = a
and A5:
b9 = b
and A6:
c9 = c
;
( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) )A7:
[a,b] in dom the
Arrows of
C1
by A1, ZFMISC_1:def 2;
A8:
[b,c] in dom the
Arrows of
C1
by A1, ZFMISC_1:def 2;
thus A9:
<^a,b^> =
(~ the Arrows of C1) . (
b,
a)
by A7, FUNCT_4:def 2
.=
<^b9,a9^>
by A3, A4, A5
;
( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f )A10:
<^b,c^> =
(~ the Arrows of C1) . (
c,
b)
by A8, FUNCT_4:def 2
.=
<^c9,b9^>
by A3, A5, A6
;
A11:
the
Comp of
C2 . (
c9,
b9,
a9)
= ~ ( the Comp of C1 . (a,b,c))
by A3, A4, A5, A6;
assume that A12:
<^a,b^> <> {}
and A13:
<^b,c^> <> {}
;
for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * flet f be
Morphism of
a,
b;
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * flet g be
Morphism of
b,
c;
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f
<^a,c^> <> {}
by A12, A13, ALTCAT_1:def 2;
then
dom ( the Comp of C1 . (a,b,c)) = [:( the Arrows of C1 . (b,c)),( the Arrows of C1 . (a,b)):]
by FUNCT_2:def 1;
then A14:
[g,f] in dom ( the Comp of C1 . (a,b,c))
by A12, A13, ZFMISC_1:def 2;
let f9 be
Morphism of
b9,
a9;
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * flet g9 be
Morphism of
c9,
b9;
( f9 = f & g9 = g implies f9 * g9 = g * f )assume that A15:
f9 = f
and A16:
g9 = g
;
f9 * g9 = g * fthus f9 * g9 =
(~ ( the Comp of C1 . (a,b,c))) . (
f,
g)
by A9, A10, A11, A12, A13, A15, A16, ALTCAT_1:def 8
.=
( the Comp of C1 . (a,b,c)) . (
g,
f)
by A14, FUNCT_4:def 2
.=
g * f
by A12, A13, ALTCAT_1:def 8
;
verum
end;
assume that
A17:
the carrier of C2 = the carrier of C1
and
A18:
for a, b, c being Object of C1
for a9, b9, c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
( <^a,b^> = <^b9,a9^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = f & g9 = g holds
f9 * g9 = g * f ) )
; C1,C2 are_opposite
thus
the carrier of C2 = the carrier of C1
by A17; YELLOW18:def 3 ( the Arrows of C2 = ~ the Arrows of C1 & ( for a, b, c being Object of C1
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 C1 . (c,b,a)) ) )
A19:
now for x being object holds
( ( x in dom the Arrows of C2 implies ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 ) ) & ( ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 ) implies x in dom the Arrows of C2 ) )let x be
object ;
( ( x in dom the Arrows of C2 implies ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 ) ) & ( ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 ) implies x in dom the Arrows of C2 ) )hereby ( ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 ) implies x in dom the Arrows of C2 )
assume
x in dom the
Arrows of
C2
;
ex z, y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 )then consider y,
z being
object such that A20:
y in the
carrier of
C1
and A21:
z in the
carrier of
C1
and A22:
[y,z] = x
by A17, ZFMISC_1:def 2;
take z =
z;
ex y being object st
( x = [y,z] & [z,y] in dom the Arrows of C1 )take y =
y;
( x = [y,z] & [z,y] in dom the Arrows of C1 )thus
(
x = [y,z] &
[z,y] in dom the
Arrows of
C1 )
by A1, A20, A21, A22, ZFMISC_1:def 2;
verum
end; given z,
y being
object such that A23:
x = [y,z]
and A24:
[z,y] in dom the
Arrows of
C1
;
x in dom the Arrows of C2A25:
z in the
carrier of
C1
by A24, ZFMISC_1:87;
y in the
carrier of
C1
by A24, ZFMISC_1:87;
hence
x in dom the
Arrows of
C2
by A2, A17, A23, A25, ZFMISC_1:def 2;
verum end;
now for y, z being object st [y,z] in dom the Arrows of C1 holds
the Arrows of C2 . (z,y) = the Arrows of C1 . (y,z)let y,
z be
object ;
( [y,z] in dom the Arrows of C1 implies the Arrows of C2 . (z,y) = the Arrows of C1 . (y,z) )assume
[y,z] in dom the
Arrows of
C1
;
the Arrows of C2 . (z,y) = the Arrows of C1 . (y,z)then reconsider a =
y,
b =
z as
Object of
C1 by ZFMISC_1:87;
reconsider a9 =
a,
b9 =
b as
Object of
C2 by A17;
thus the
Arrows of
C2 . (
z,
y) =
<^b9,a9^>
.=
<^a,b^>
by A18
.=
the
Arrows of
C1 . (
y,
z)
;
verum end;
hence
the Arrows of C2 = ~ the Arrows of C1
by A19, FUNCT_4:def 2; for a, b, c being Object of C1
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 C1 . (c,b,a))
let a, b, c be Object of C1; 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 C1 . (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 C1 . (c,b,a)) )
assume that
A26:
a9 = a
and
A27:
b9 = b
and
A28:
c9 = c
; the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a))
A29:
<^a9,b9^> = <^b,a^>
by A18, A26, A27;
A30:
<^b9,c9^> = <^c,b^>
by A18, A27, A28;
A31:
<^a9,c9^> = <^c,a^>
by A18, A26, A28;
( [:<^b,a^>,<^c,b^>:] <> {} implies ( <^b,a^> <> {} & <^c,b^> <> {} ) )
by ZFMISC_1:90;
then
( [:<^b,a^>,<^c,b^>:] <> {} implies <^c,a^> <> {} )
by ALTCAT_1:def 2;
then A32:
dom ( the Comp of C1 . (c,b,a)) = [:( the Arrows of C1 . (b,a)),( the Arrows of C1 . (c,b)):]
by FUNCT_2:def 1;
( [:<^c,b^>,<^b,a^>:] <> {} implies ( <^b,a^> <> {} & <^c,b^> <> {} ) )
by ZFMISC_1:90;
then
( [:<^c,b^>,<^b,a^>:] <> {} implies <^c,a^> <> {} )
by ALTCAT_1:def 2;
then A33:
dom ( the Comp of C2 . (a9,b9,c9)) = [:( the Arrows of C2 . (b9,c9)),( the Arrows of C2 . (a9,b9)):]
by A29, A30, A31, FUNCT_2:def 1;
A34:
now for x being object holds
( ( x in dom ( the Comp of C2 . (a9,b9,c9)) implies ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) ) ) & ( ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) ) implies x in dom ( the Comp of C2 . (a9,b9,c9)) ) )let x be
object ;
( ( x in dom ( the Comp of C2 . (a9,b9,c9)) implies ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) ) ) & ( ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) ) implies x in dom ( the Comp of C2 . (a9,b9,c9)) ) )hereby ( ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) ) implies x in dom ( the Comp of C2 . (a9,b9,c9)) )
assume
x in dom ( the Comp of C2 . (a9,b9,c9))
;
ex z, y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) )then consider y,
z being
object such that A35:
y in <^b9,c9^>
and A36:
z in <^a9,b9^>
and A37:
[y,z] = x
by ZFMISC_1:def 2;
take z =
z;
ex y being object st
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) )take y =
y;
( x = [y,z] & [z,y] in dom ( the Comp of C1 . (c,b,a)) )thus
(
x = [y,z] &
[z,y] in dom ( the Comp of C1 . (c,b,a)) )
by A29, A30, A32, A35, A36, A37, ZFMISC_1:def 2;
verum
end; given z,
y being
object such that A38:
x = [y,z]
and A39:
[z,y] in dom ( the Comp of C1 . (c,b,a))
;
x in dom ( the Comp of C2 . (a9,b9,c9))A40:
z in <^b,a^>
by A39, ZFMISC_1:87;
y in <^c,b^>
by A39, ZFMISC_1:87;
hence
x in dom ( the Comp of C2 . (a9,b9,c9))
by A29, A30, A33, A38, A40, ZFMISC_1:def 2;
verum end;
now for y, z being object st [y,z] in dom ( the Comp of C1 . (c,b,a)) holds
( the Comp of C2 . (a9,b9,c9)) . (z,y) = ( the Comp of C1 . (c,b,a)) . (y,z)let y,
z be
object ;
( [y,z] in dom ( the Comp of C1 . (c,b,a)) implies ( the Comp of C2 . (a9,b9,c9)) . (z,y) = ( the Comp of C1 . (c,b,a)) . (y,z) )assume A41:
[y,z] in dom ( the Comp of C1 . (c,b,a))
;
( the Comp of C2 . (a9,b9,c9)) . (z,y) = ( the Comp of C1 . (c,b,a)) . (y,z)then A42:
y in <^b,a^>
by ZFMISC_1:87;
A43:
z in <^c,b^>
by A41, ZFMISC_1:87;
reconsider f =
y as
Morphism of
b,
a by A41, ZFMISC_1:87;
reconsider g =
z as
Morphism of
c,
b by A41, ZFMISC_1:87;
reconsider f9 =
y as
Morphism of
a9,
b9 by A18, A26, A27, A42;
reconsider g9 =
z as
Morphism of
b9,
c9 by A18, A27, A28, A43;
thus ( the Comp of C2 . (a9,b9,c9)) . (
z,
y) =
g9 * f9
by A29, A30, A42, A43, ALTCAT_1:def 8
.=
f * g
by A18, A26, A27, A28, A42, A43
.=
( the Comp of C1 . (c,b,a)) . (
y,
z)
by A42, A43, ALTCAT_1:def 8
;
verum end;
hence
the Comp of C2 . (a9,b9,c9) = ~ ( the Comp of C1 . (c,b,a))
by A34, FUNCT_4:def 2; verum