begin
theorem Th10:
for
i,
j,
k being
set holds
((i,j) :-> k) . (
i,
j)
= k
begin
begin
definition
let I be
set ;
let G be
ManySortedSet of
[:I,I:];
existence
ex b1 being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
b1 . (i,j,k) = G . (i,k)
uniqueness
for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being set st i in I & j in I & k in I holds
b1 . (i,j,k) = G . (i,k) ) & ( for i, j, k being set st i in I & j in I & k in I holds
b2 . (i,j,k) = G . (i,k) ) holds
b1 = b2
let H be
ManySortedSet of
[:I,I:];
func {|G,H|} -> ManySortedSet of
[:I,I,I:] means :
Def4:
for
i,
j,
k being
set st
i in I &
j in I &
k in I holds
it . (
i,
j,
k)
= [:(H . (j,k)),(G . (i,j)):];
existence
ex b1 being ManySortedSet of [:I,I,I:] st
for i, j, k being set st i in I & j in I & k in I holds
b1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):]
uniqueness
for b1, b2 being ManySortedSet of [:I,I,I:] st ( for i, j, k being set st i in I & j in I & k in I holds
b1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) & ( for i, j, k being set st i in I & j in I & k in I holds
b2 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] ) holds
b1 = b2
end;
::
deftheorem Def4 defines
{| ALTCAT_1:def 4 :
for I being set
for G, H being ManySortedSet of [:I,I:]
for b4 being ManySortedSet of [:I,I,I:] holds
( b4 = {|G,H|} iff for i, j, k being set st i in I & j in I & k in I holds
b4 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] );
definition
let I be non
empty set ;
let G be
ManySortedSet of
[:I,I:];
let o be
BinComp of
G;
let i,
j,
k be
Element of
I;
.redefine func o . (
i,
j,
k)
-> Function of
[:(G . (j,k)),(G . (i,j)):],
(G . (i,k));
coherence
o . (i,j,k) is Function of [:(G . (j,k)),(G . (i,j)):],(G . (i,k))
end;
definition
let I be non
empty set ;
let G be
ManySortedSet of
[:I,I:];
let IT be
BinComp of
G;
attr IT is
associative means :
Def5:
for
i,
j,
k,
l being
Element of
I for
f,
g,
h being
set st
f in G . (
i,
j) &
g in G . (
j,
k) &
h in G . (
k,
l) holds
(IT . (i,k,l)) . (
h,
((IT . (i,j,k)) . (g,f)))
= (IT . (i,j,l)) . (
((IT . (j,k,l)) . (h,g)),
f);
end;
::
deftheorem Def5 defines
associative ALTCAT_1:def 5 :
for I being non empty set
for G being ManySortedSet of [:I,I:]
for IT being BinComp of G holds
( IT is associative iff for i, j, k, l being Element of I
for f, g, h being set st f in G . (i,j) & g in G . (j,k) & h in G . (k,l) holds
(IT . (i,k,l)) . (h,((IT . (i,j,k)) . (g,f))) = (IT . (i,j,l)) . (((IT . (j,k,l)) . (h,g)),f) );
begin
definition
let C be non
empty AltCatStr ;
let o1,
o2,
o3 be
object of
C;
assume A1:
(
<^o1,o2^> <> {} &
<^o2,o3^> <> {} )
;
let f be
Morphism of
o1,
o2;
let g be
Morphism of
o2,
o3;
coherence
( the Comp of C . (o1,o2,o3)) . (g,f) is Morphism of o1,o3
correctness
;
end;
definition
let C be non
empty AltCatStr ;
attr C is
pseudo-functional means :
Def13:
for
o1,
o2,
o3 being
object of
C holds the
Comp of
C . (
o1,
o2,
o3)
= (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:];
end;
::
deftheorem Def13 defines
pseudo-functional ALTCAT_1:def 13 :
for C being non empty AltCatStr holds
( C is pseudo-functional iff for o1, o2, o3 being object of C holds the Comp of C . (o1,o2,o3) = (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] );
definition
let A be non
empty set ;
existence
ex b1 being non empty strict pseudo-functional AltCatStr st
( the carrier of b1 = A & ( for a1, a2 being object of b1 holds <^a1,a2^> = Funcs (a1,a2) ) )
uniqueness
for b1, b2 being non empty strict pseudo-functional AltCatStr st the carrier of b1 = A & ( for a1, a2 being object of b1 holds <^a1,a2^> = Funcs (a1,a2) ) & the carrier of b2 = A & ( for a1, a2 being object of b2 holds <^a1,a2^> = Funcs (a1,a2) ) holds
b1 = b2
end;
Lm1:
for A being non empty set holds
( EnsCat A is transitive & EnsCat A is associative & EnsCat A is with_units )
theorem
for
C being non
empty transitive AltCatStr for
a1,
a2,
a3 being
object of
C holds
(
dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] &
rng ( the Comp of C . (a1,a2,a3)) c= <^a1,a3^> )
begin
begin