catalg_1.miz
begin
definition
let I be
set;
let A,f be
Function;
::
CATALG_1:def1
func f
-MSF (I,A) ->
ManySortedFunction of I means
:
Def1: for i be
object st i
in I holds (it
. i)
= (f
| (A
. i));
existence
proof
deffunc
f(
object) = (f
| (A
. $1));
consider F be
ManySortedSet of I such that
A1: for i be
object st i
in I holds (F
. i)
=
f(i) from
PBOOLE:sch 4;
F is
Function-yielding
proof
let x be
object;
assume x
in (
dom F);
then x
in I;
then (F
. x)
= (f
| (A
. x)) by
A1;
hence thesis;
end;
hence thesis by
A1;
end;
uniqueness
proof
let g1,g2 be
ManySortedFunction of I such that
A2: for i be
object st i
in I holds (g1
. i)
= (f
| (A
. i)) and
A3: for i be
object st i
in I holds (g2
. i)
= (f
| (A
. i));
now
let i be
object;
assume
A4: i
in I;
then (g1
. i)
= (f
| (A
. i)) by
A2;
hence (g1
. i)
= (g2
. i) by
A3,
A4;
end;
hence thesis;
end;
end
theorem ::
CATALG_1:1
for I be
set, A be
ManySortedSet of I holds ((
id (
Union A))
-MSF (I,A))
= (
id A)
proof
let I be
set, A be
ManySortedSet of I;
set f = (
id (
Union A)), F = (f
-MSF (I,A));
now
let i be
object;
A1: (
Union A)
= (
union (
rng A)) by
CARD_3:def 4;
assume
A2: i
in I;
then i
in (
dom A) by
PARTFUN1:def 2;
then
A3: (A
. i)
in (
rng A) by
FUNCT_1:def 3;
(F
. i)
= (f
| (A
. i)) & ((
id A)
. i)
= (
id (A
. i)) by
A2,
Def1,
MSUALG_3:def 1;
hence (F
. i)
= ((
id A)
. i) by
A3,
A1,
FUNCT_3: 1,
ZFMISC_1: 74;
end;
hence thesis;
end;
theorem ::
CATALG_1:2
for I be
set, A,B be
ManySortedSet of I holds for f,g be
Function st (
rngs (f
-MSF (I,A)))
c= B holds ((g
* f)
-MSF (I,A))
= ((g
-MSF (I,B))
** (f
-MSF (I,A)))
proof
let I be
set, A,B be
ManySortedSet of I;
let f,g be
Function such that
A1: (
rngs (f
-MSF (I,A)))
c= B;
A2: (I
/\ I)
= I;
(
dom (g
-MSF (I,B)))
= I & (
dom (f
-MSF (I,A)))
= I by
PARTFUN1:def 2;
then
A3: (
dom ((g
-MSF (I,B))
** (f
-MSF (I,A))))
= I by
A2,
PBOOLE:def 19;
A4:
now
let i be
object;
assume
A5: i
in I;
then
A6: ((f
-MSF (I,A))
. i)
= (f
| (A
. i)) by
Def1;
(
dom (f
-MSF (I,A)))
= I by
PARTFUN1:def 2;
then ((
rngs (f
-MSF (I,A)))
. i)
= (
rng (f
| (A
. i))) by
A5,
A6,
FUNCT_6: 22;
then (
rng (f
| (A
. i)))
c= (B
. i) by
A1,
A5;
then ((g
* f)
| (A
. i))
= (g
* (f
| (A
. i))) & ((B
. i)
|` (f
| (A
. i)))
= (f
| (A
. i)) by
RELAT_1: 83,
RELAT_1: 94;
then
A7: ((g
* f)
| (A
. i))
= ((g
| (B
. i))
* (f
| (A
. i))) by
MONOID_1: 1;
(((g
* f)
-MSF (I,A))
. i)
= ((g
* f)
| (A
. i)) & ((g
-MSF (I,B))
. i)
= (g
| (B
. i)) by
A5,
Def1;
hence (((g
* f)
-MSF (I,A))
. i)
= (((g
-MSF (I,B))
** (f
-MSF (I,A)))
. i) by
A3,
A5,
A6,
A7,
PBOOLE:def 19;
end;
(
dom ((g
* f)
-MSF (I,A)))
= I by
PARTFUN1:def 2;
hence thesis by
A3,
A4,
FUNCT_1: 2;
end;
theorem ::
CATALG_1:3
for f be
Function, I be
set holds for A,B be
ManySortedSet of I st for i be
set st i
in I holds (A
. i)
c= (
dom f) & (f
.: (A
. i))
c= (B
. i) holds (f
-MSF (I,A)) is
ManySortedFunction of A, B
proof
let f be
Function, I be
set;
let A,B be
ManySortedSet of I such that
A1: for i be
set st i
in I holds (A
. i)
c= (
dom f) & (f
.: (A
. i))
c= (B
. i);
let i be
object;
assume
A2: i
in I;
then
A3: ((f
-MSF (I,A))
. i)
= (f
| (A
. i)) by
Def1;
(f
.: (A
. i))
c= (B
. i) by
A1,
A2;
then
A4: (
rng ((f
-MSF (I,A))
. i))
c= (B
. i) by
A3,
RELAT_1: 115;
(
dom ((f
-MSF (I,A))
. i))
= (A
. i) by
A1,
A2,
A3,
RELAT_1: 62;
hence thesis by
A4,
FUNCT_2: 2;
end;
Lm1:
now
let x,y be
set;
assume
<*x*>
=
<*y*>;
then (
<*x*>
. 1)
= y by
FINSEQ_1: 40;
hence x
= y by
FINSEQ_1: 40;
end;
definition
let S be non
empty
ManySortedSign;
let A be
MSAlgebra over S;
::
CATALG_1:def2
attr A is
empty means
:
Def2: the
Sorts of A is
empty-yielding;
end
registration
let S be non
empty
ManySortedSign;
cluster
non-empty -> non
empty for
MSAlgebra over S;
coherence ;
end
registration
let S be non
empty non
void
ManySortedSign;
cluster
strict
non-empty
disjoint_valued for
MSAlgebra over S;
existence
proof
set X = the
non-empty
ManySortedSet of the
carrier of S;
take (
FreeMSA X);
thus thesis;
end;
end
registration
let S be non
empty non
void
ManySortedSign;
let A be non
empty
MSAlgebra over S;
cluster the
Sorts of A -> non
empty-yielding;
coherence by
Def2;
end
registration
cluster non
empty-yielding for
Function;
existence
proof
set S = the non
empty non
void
ManySortedSign;
set A = the non
empty
MSAlgebra over S;
take the
Sorts of A;
thus thesis;
end;
end
begin
definition
let A be
set;
::
CATALG_1:def3
func
CatSign A ->
strict
ManySortedSign means
:
Def3: the
carrier of it
=
[:
{
0 }, (2
-tuples_on A):] & the
carrier' of it
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) & (for a be
set st a
in A holds (the
Arity of it
.
[1,
<*a*>])
=
{} & (the
ResultSort of it
.
[1,
<*a*>])
=
[
0 ,
<*a, a*>]) & for a,b,c be
set st a
in A & b
in A & c
in A holds (the
Arity of it
.
[2,
<*a, b, c*>])
=
<*
[
0 ,
<*b, c*>],
[
0 ,
<*a, b*>]*> & (the
ResultSort of it
.
[2,
<*a, b, c*>])
=
[
0 ,
<*a, c*>];
existence
proof
defpred
R[
object,
object] means ex y1,y2,y3 be
set st y1
in A & y2
in A & y3
in A & ($1
=
[1,
<*y1*>] & $2
=
[
0 ,
<*y1, y1*>] or $1
=
[2,
<*y1, y2, y3*>] & $2
=
[
0 ,
<*y1, y3*>]);
defpred
P[
object,
object] means ex y1,y2,y3 be
set st y1
in A & y2
in A & y3
in A & ($1
=
[1,
<*y1*>] & $2
=
{} or $1
=
[2,
<*y1, y2, y3*>] & $2
=
<*
[
0 ,
<*y2, y3*>],
[
0 ,
<*y1, y2*>]*>);
A1: for x be
object st x
in (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) holds ex y be
object st y
in (
[:
{
0 }, (2
-tuples_on A):]
* ) &
P[x, y]
proof
let x be
object;
assume
A2: x
in (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]);
per cases by
A2,
XBOOLE_0:def 3;
suppose
A3: x
in
[:
{1}, (1
-tuples_on A):];
then (x
`2 )
in (1
-tuples_on A) by
MCART_1: 10;
then
A4: (x
`2 )
in { s where s be
Element of (A
* ) : (
len s)
= 1 } by
FINSEQ_2:def 4;
take y =
{} ;
thus y
in (
[:
{
0 }, (2
-tuples_on A):]
* ) by
FINSEQ_1: 49;
consider s be
Element of (A
* ) such that
A5: (x
`2 )
= s and
A6: (
len s)
= 1 by
A4;
take y1 = (s
. 1), y2 = (s
. 1), y3 = (s
. 1);
A7: s
=
<*y1*> by
A6,
FINSEQ_1: 40;
then y1
in
{y1} & (
rng s)
=
{y1} by
FINSEQ_1: 39,
TARSKI:def 1;
hence y1
in A & y2
in A & y3
in A;
(x
`1 )
in
{1} by
A3,
MCART_1: 10;
then (x
`1 )
= 1 by
TARSKI:def 1;
hence thesis by
A3,
A5,
A7,
MCART_1: 21;
end;
suppose
A8: x
in
[:
{2}, (3
-tuples_on A):];
then (x
`2 )
in (3
-tuples_on A) by
MCART_1: 10;
then (x
`2 )
in { s where s be
Element of (A
* ) : (
len s)
= 3 } by
FINSEQ_2:def 4;
then
consider s be
Element of (A
* ) such that
A9: (x
`2 )
= s and
A10: (
len s)
= 3;
set y1 = (s
. 1), y2 = (s
. 2), y3 = (s
. 3);
A11: s
=
<*y1, y2, y3*> by
A10,
FINSEQ_1: 45;
then
A12: (
rng s)
=
{y1, y2, y3} by
FINSEQ_2: 128;
then
reconsider B = A as non
empty
set;
take y =
<*
[
0 ,
<*y2, y3*>],
[
0 ,
<*y1, y2*>]*>;
A13: y2
in
{y1, y2, y3} by
ENUMSET1:def 1;
A14: y1
in
{y1, y2, y3} by
ENUMSET1:def 1;
then
A15:
0
in
{
0 } &
<*y1, y2*>
in (2
-tuples_on B) by
A13,
A12,
FINSEQ_2: 101,
TARSKI:def 1;
A16: y3
in
{y1, y2, y3} by
ENUMSET1:def 1;
then
<*y2, y3*>
in (2
-tuples_on B) by
A13,
A12,
FINSEQ_2: 101;
then
reconsider z1 =
[
0 ,
<*y2, y3*>], z2 =
[
0 ,
<*y1, y2*>] as
Element of
[:
{
0 }, (2
-tuples_on B):] by
A15,
ZFMISC_1: 87;
y
= (
<*z1*>
^
<*z2*>) by
FINSEQ_1:def 9;
hence y
in (
[:
{
0 }, (2
-tuples_on A):]
* ) by
FINSEQ_1:def 11;
take y1, y2, y3;
thus y1
in A & y2
in A & y3
in A by
A14,
A13,
A16,
A12;
(x
`1 )
in
{2} by
A8,
MCART_1: 10;
then (x
`1 )
= 2 by
TARSKI:def 1;
hence thesis by
A8,
A9,
A11,
MCART_1: 21;
end;
end;
consider Ar be
Function such that
A17: (
dom Ar)
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) & (
rng Ar)
c= (
[:
{
0 }, (2
-tuples_on A):]
* ) and
A18: for x be
object st x
in (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) holds
P[x, (Ar
. x)] from
FUNCT_1:sch 6(
A1);
reconsider Ar as
Function of (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]), (
[:
{
0 }, (2
-tuples_on A):]
* ) by
A17,
FUNCT_2: 2;
A19: for x be
object st x
in (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) holds ex y be
object st y
in
[:
{
0 }, (2
-tuples_on A):] &
R[x, y]
proof
let x be
object;
assume
A20: x
in (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]);
per cases by
A20,
XBOOLE_0:def 3;
suppose
A21: x
in
[:
{1}, (1
-tuples_on A):];
then (x
`2 )
in (1
-tuples_on A) by
MCART_1: 10;
then (x
`2 )
in { s where s be
Element of (A
* ) : (
len s)
= 1 } by
FINSEQ_2:def 4;
then
consider s be
Element of (A
* ) such that
A22: (x
`2 )
= s and
A23: (
len s)
= 1;
set y1 = (s
. 1), y2 = (s
. 1), y3 = (s
. 1);
A24: s
=
<*y1*> by
A23,
FINSEQ_1: 40;
then
A25: y1
in
{y1} & (
rng s)
=
{y1} by
FINSEQ_1: 39,
TARSKI:def 1;
take y =
[
0 ,
<*y1, y1*>];
reconsider B = A as non
empty
set by
A24;
reconsider y1 as
Element of B by
A25;
0
in
{
0 } &
<*y1, y1*>
in (2
-tuples_on B) by
FINSEQ_2: 101,
TARSKI:def 1;
hence y
in
[:
{
0 }, (2
-tuples_on A):] by
ZFMISC_1: 87;
take y1, y2, y3;
thus y1
in A & y2
in A & y3
in A by
A25;
(x
`1 )
in
{1} by
A21,
MCART_1: 10;
then (x
`1 )
= 1 by
TARSKI:def 1;
hence x
=
[1,
<*y1*>] & y
=
[
0 ,
<*y1, y1*>] or x
=
[2,
<*y1, y2, y3*>] & y
=
[
0 ,
<*y1, y3*>] by
A21,
A22,
A24,
MCART_1: 21;
end;
suppose
A26: x
in
[:
{2}, (3
-tuples_on A):];
then (x
`2 )
in (3
-tuples_on A) by
MCART_1: 10;
then (x
`2 )
in { s where s be
Element of (A
* ) : (
len s)
= 3 } by
FINSEQ_2:def 4;
then
consider s be
Element of (A
* ) such that
A27: (x
`2 )
= s and
A28: (
len s)
= 3;
set y1 = (s
. 1), y2 = (s
. 2), y3 = (s
. 3);
A29: s
=
<*y1, y2, y3*> by
A28,
FINSEQ_1: 45;
then
A30: (
rng s)
=
{y1, y2, y3} by
FINSEQ_2: 128;
then
reconsider B = A as non
empty
set;
take y =
[
0 ,
<*y1, y3*>];
A31: y1
in
{y1, y2, y3} & y3
in
{y1, y2, y3} by
ENUMSET1:def 1;
then
0
in
{
0 } &
<*y1, y3*>
in (2
-tuples_on B) by
A30,
FINSEQ_2: 101,
TARSKI:def 1;
hence y
in
[:
{
0 }, (2
-tuples_on A):] by
ZFMISC_1: 87;
take y1, y2, y3;
y2
in
{y1, y2, y3} by
ENUMSET1:def 1;
hence y1
in A & y2
in A & y3
in A by
A31,
A30;
(x
`1 )
in
{2} by
A26,
MCART_1: 10;
then (x
`1 )
= 2 by
TARSKI:def 1;
hence thesis by
A26,
A27,
A29,
MCART_1: 21;
end;
end;
consider R be
Function such that
A32: (
dom R)
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) & (
rng R)
c=
[:
{
0 }, (2
-tuples_on A):] and
A33: for x be
object st x
in (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) holds
R[x, (R
. x)] from
FUNCT_1:sch 6(
A19);
reconsider R as
Function of (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]),
[:
{
0 }, (2
-tuples_on A):] by
A32,
FUNCT_2: 2;
take S =
ManySortedSign (#
[:
{
0 }, (2
-tuples_on A):], (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]), Ar, R #);
thus the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):];
thus the
carrier' of S
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]);
hereby
let a be
set;
assume
A34: a
in A;
then
reconsider B = A as non
empty
set;
reconsider x = a as
Element of B by
A34;
<*x*> is
Element of (1
-tuples_on B) & 1
in
{1} by
FINSEQ_2: 98,
TARSKI:def 1;
then
[1,
<*a*>]
in
[:
{1}, (1
-tuples_on A):] by
ZFMISC_1: 87;
then
A35:
[1,
<*a*>]
in (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
XBOOLE_0:def 3;
then
consider y1,y2,y3 be
set such that y1
in A and y2
in A and y3
in A and
A36:
[1,
<*a*>]
=
[1,
<*y1*>] & (R
.
[1,
<*a*>])
=
[
0 ,
<*y1, y1*>] or
[1,
<*a*>]
=
[2,
<*y1, y2, y3*>] & (R
.
[1,
<*a*>])
=
[
0 ,
<*y1, y3*>] by
A33;
ex y1,y2,y3 be
set st y1
in A & y2
in A & y3
in A & (
[1,
<*a*>]
=
[1,
<*y1*>] & (Ar
.
[1,
<*a*>])
=
{} or
[1,
<*a*>]
=
[2,
<*y1, y2, y3*>] & (Ar
.
[1,
<*a*>])
=
<*
[
0 ,
<*y2, y3*>],
[
0 ,
<*y1, y2*>]*>) by
A18,
A35;
hence (the
Arity of S
.
[1,
<*a*>])
=
{} by
XTUPLE_0: 1;
A37: (
<*a*>
. 1)
= a & (
<*y1*>
. 1)
= y1 by
FINSEQ_1: 40;
<*a*>
=
<*y1*> by
A36,
XTUPLE_0: 1;
hence (the
ResultSort of S
.
[1,
<*a*>])
=
[
0 ,
<*a, a*>] by
A36,
A37,
XTUPLE_0: 1;
end;
let a,b,c be
set;
assume that
A38: a
in A and
A39: b
in A & c
in A;
reconsider B = A as non
empty
set by
A38;
reconsider x = a, y = b, z = c as
Element of B by
A38,
A39;
<*x, y, z*> is
Element of (3
-tuples_on B) & 2
in
{2} by
FINSEQ_2: 104,
TARSKI:def 1;
then
[2,
<*a, b, c*>]
in
[:
{2}, (3
-tuples_on A):] by
ZFMISC_1: 87;
then
A40:
[2,
<*a, b, c*>]
in (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
XBOOLE_0:def 3;
then
consider y1,y2,y3 be
set such that y1
in A and y2
in A and y3
in A and
A41:
[2,
<*a, b, c*>]
=
[1,
<*y1*>] & (Ar
.
[2,
<*a, b, c*>])
=
{} or
[2,
<*a, b, c*>]
=
[2,
<*y1, y2, y3*>] & (Ar
.
[2,
<*a, b, c*>])
=
<*
[
0 ,
<*y2, y3*>],
[
0 ,
<*y1, y2*>]*> by
A18;
A42:
<*a, b, c*>
= ((
<*a*>
^
<*b*>)
^
<*c*>) &
<*y1, y2, y3*>
= ((
<*y1*>
^
<*y2*>)
^
<*y3*>) by
FINSEQ_1:def 10;
A43:
<*a, b, c*>
=
<*y1, y2, y3*> by
A41,
XTUPLE_0: 1;
then
A44: (
<*a*>
^
<*b*>)
= (
<*y1*>
^
<*y2*>) by
A42,
FINSEQ_2: 17;
then
<*a*>
=
<*y1*> by
FINSEQ_2: 17;
then
A45: a
= y1 by
Lm1;
b
= y2 by
A44,
FINSEQ_2: 17;
hence (the
Arity of S
.
[2,
<*a, b, c*>])
=
<*
[
0 ,
<*b, c*>],
[
0 ,
<*a, b*>]*> by
A41,
A43,
A42,
A45,
FINSEQ_2: 17,
XTUPLE_0: 1;
consider y1,y2,y3 be
set such that y1
in A and y2
in A and y3
in A and
A46:
[2,
<*a, b, c*>]
=
[1,
<*y1*>] & (R
.
[2,
<*a, b, c*>])
=
[
0 ,
<*y1, y1*>] or
[2,
<*a, b, c*>]
=
[2,
<*y1, y2, y3*>] & (R
.
[2,
<*a, b, c*>])
=
[
0 ,
<*y1, y3*>] by
A33,
A40;
A47: (
<*a, b, c*>
. 1)
= a & (
<*y1, y2, y3*>
. 1)
= y1 by
FINSEQ_1: 45;
A48: (
<*a, b, c*>
. 3)
= c by
FINSEQ_1: 45;
<*a, b, c*>
=
<*y1, y2, y3*> by
A46,
XTUPLE_0: 1;
hence thesis by
A46,
A47,
A48,
FINSEQ_1: 45,
XTUPLE_0: 1;
end;
correctness
proof
let S1,S2 be
strict
ManySortedSign such that
A49: the
carrier of S1
=
[:
{
0 }, (2
-tuples_on A):] and
A50: the
carrier' of S1
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) and
A51: for a be
set st a
in A holds (the
Arity of S1
.
[1,
<*a*>])
=
{} & (the
ResultSort of S1
.
[1,
<*a*>])
=
[
0 ,
<*a, a*>] and
A52: for a,b,c be
set st a
in A & b
in A & c
in A holds (the
Arity of S1
.
[2,
<*a, b, c*>])
=
<*
[
0 ,
<*b, c*>],
[
0 ,
<*a, b*>]*> & (the
ResultSort of S1
.
[2,
<*a, b, c*>])
=
[
0 ,
<*a, c*>] and
A53: the
carrier of S2
=
[:
{
0 }, (2
-tuples_on A):] and
A54: the
carrier' of S2
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) and
A55: for a be
set st a
in A holds (the
Arity of S2
.
[1,
<*a*>])
=
{} & (the
ResultSort of S2
.
[1,
<*a*>])
=
[
0 ,
<*a, a*>] and
A56: for a,b,c be
set st a
in A & b
in A & c
in A holds (the
Arity of S2
.
[2,
<*a, b, c*>])
=
<*
[
0 ,
<*b, c*>],
[
0 ,
<*a, b*>]*> & (the
ResultSort of S2
.
[2,
<*a, b, c*>])
=
[
0 ,
<*a, c*>];
A57:
now
let x be
object;
assume x
in (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]);
then
A58: x
in
[:
{1}, (1
-tuples_on A):] or x
in
[:
{2}, (3
-tuples_on A):] by
XBOOLE_0:def 3;
then (x
`1 )
in
{1} & (x
`2 )
in (1
-tuples_on A) or (x
`1 )
in
{2} & (x
`2 )
in (3
-tuples_on A) by
MCART_1: 10;
then
A59: (x
`1 )
= 1 & (x
`2 )
in (1
-tuples_on A) or (x
`1 )
= 2 & (x
`2 )
in (3
-tuples_on A) by
TARSKI:def 1;
A60:
now
assume (x
`2 )
in (3
-tuples_on A);
then
consider a,b,c be
object such that
A61: a
in A & b
in A & c
in A & (x
`2 )
=
<*a, b, c*> by
FINSEQ_2: 139;
thus (the
Arity of S1
.
[2, (x
`2 )])
=
<*
[
0 ,
<*b, c*>],
[
0 ,
<*a, b*>]*> by
A52,
A61
.= (the
Arity of S2
.
[2, (x
`2 )]) by
A56,
A61;
end;
A62:
now
assume (x
`2 )
in (1
-tuples_on A);
then
A63: ex a be
set st a
in A & (x
`2 )
=
<*a*> by
FINSEQ_2: 135;
hence (the
Arity of S1
.
[1, (x
`2 )])
=
{} by
A51
.= (the
Arity of S2
.
[1, (x
`2 )]) by
A55,
A63;
end;
x
=
[(x
`1 ), (x
`2 )] by
A58,
MCART_1: 21;
hence (the
Arity of S1
. x)
= (the
Arity of S2
. x) by
A59,
A62,
A60;
end;
A64:
now
let x be
object;
assume x
in (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]);
then
A65: x
in
[:
{1}, (1
-tuples_on A):] or x
in
[:
{2}, (3
-tuples_on A):] by
XBOOLE_0:def 3;
then (x
`1 )
in
{1} & (x
`2 )
in (1
-tuples_on A) or (x
`1 )
in
{2} & (x
`2 )
in (3
-tuples_on A) by
MCART_1: 10;
then
A66: (x
`1 )
= 1 & (x
`2 )
in (1
-tuples_on A) or (x
`1 )
= 2 & (x
`2 )
in (3
-tuples_on A) by
TARSKI:def 1;
A67:
now
assume (x
`2 )
in (3
-tuples_on A);
then
consider a,b,c be
object such that
A68: a
in A & b
in A & c
in A & (x
`2 )
=
<*a, b, c*> by
FINSEQ_2: 139;
thus (the
ResultSort of S1
.
[2, (x
`2 )])
=
[
0 ,
<*a, c*>] by
A52,
A68
.= (the
ResultSort of S2
.
[2, (x
`2 )]) by
A56,
A68;
end;
A69:
now
assume (x
`2 )
in (1
-tuples_on A);
then
consider a be
set such that
A70: a
in A & (x
`2 )
=
<*a*> by
FINSEQ_2: 135;
thus (the
ResultSort of S1
.
[1, (x
`2 )])
=
[
0 ,
<*a, a*>] by
A51,
A70
.= (the
ResultSort of S2
.
[1, (x
`2 )]) by
A55,
A70;
end;
x
=
[(x
`1 ), (x
`2 )] by
A65,
MCART_1: 21;
hence (the
ResultSort of S1
. x)
= (the
ResultSort of S2
. x) by
A66,
A69,
A67;
end;
(
dom the
Arity of S1)
= the
carrier' of S1 & (
dom the
Arity of S2)
= the
carrier' of S2 by
FUNCT_2:def 1;
then
A71: the
Arity of S1
= the
Arity of S2 by
A50,
A54,
A57,
FUNCT_1: 2;
now
assume
[:
{
0 }, (2
-tuples_on A):]
=
{} ;
then A
=
{} ;
then
A72: 1
<>
0 & 3
<>
0 implies (1
-tuples_on A)
=
{} & (3
-tuples_on A)
=
{} by
FINSEQ_3: 119;
then
[:
{1}, (1
-tuples_on A):]
=
{} by
ZFMISC_1: 90;
hence (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):])
=
{} by
A72,
ZFMISC_1: 90;
end;
then (
dom the
ResultSort of S1)
= the
carrier' of S1 & (
dom the
ResultSort of S2)
= the
carrier' of S2 by
A49,
A50,
A53,
A54,
FUNCT_2:def 1;
hence thesis by
A49,
A50,
A53,
A54,
A71,
A64,
FUNCT_1: 2;
end;
end
registration
let A be
set;
cluster (
CatSign A) ->
feasible;
coherence
proof
assume the
carrier of (
CatSign A)
=
{} ;
then
[:
{
0 }, (2
-tuples_on A):]
=
{} by
Def3;
then A
=
{} ;
then
A1: 1
<>
0 & 3
<>
0 implies (1
-tuples_on A)
=
{} & (3
-tuples_on A)
=
{} by
FINSEQ_3: 119;
then
[:
{1}, (1
-tuples_on A):]
=
{} by
ZFMISC_1: 90;
then (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):])
=
{} by
A1,
ZFMISC_1: 90;
hence thesis by
Def3;
end;
end
registration
let A be non
empty
set;
cluster (
CatSign A) -> non
empty non
void;
coherence
proof
the
carrier of (
CatSign A)
=
[:
{
0 }, (2
-tuples_on A):] by
Def3;
hence the
carrier of (
CatSign A) is non
empty;
the
carrier' of (
CatSign A)
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
Def3;
hence the
carrier' of (
CatSign A) is non
empty;
end;
end
definition
mode
Signature is
feasible
ManySortedSign;
end
definition
let S be
Signature;
::
CATALG_1:def4
attr S is
Categorial means
:
Def4: ex A be
set st (
CatSign A) is
Subsignature of S & the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):];
end
registration
cluster
Categorial -> non
void for non
empty
Signature;
coherence
proof
let S be non
empty
Signature;
given A be
set such that
A1: (
CatSign A) is
Subsignature of S and
A2: the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):];
set s = the
SortSymbol of S;
consider z,p be
object such that z
in
{
0 } and
A3: p
in (2
-tuples_on A) and s
=
[z, p] by
A2,
ZFMISC_1: 84;
(2
-tuples_on A)
= { q where q be
Element of (A
* ) : (
len q)
= 2 } by
FINSEQ_2:def 4;
then
consider q be
Element of (A
* ) such that p
= q and
A4: (
len q)
= 2 by
A3;
A5: (
dom q)
= (
Seg 2) by
A4,
FINSEQ_1:def 3;
then
reconsider A9 = A as non
empty
set;
1
in (
dom q) by
A5,
FINSEQ_1: 2,
TARSKI:def 2;
then (q
. 1)
in (
rng q) by
FUNCT_1:def 3;
then
reconsider a = (q
. 1) as
Element of A9;
the
carrier' of (
CatSign A)
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
Def3;
then
<*a*> is
Element of (1
-tuples_on A9) & (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):])
c= the
carrier' of S by
A1,
FINSEQ_2: 98,
INSTALG1: 10;
hence the
carrier' of S is non
empty;
end;
end
registration
cluster
Categorial non
empty
strict for
Signature;
existence
proof
take S = (
CatSign
{
{} });
thus S is
Categorial
proof
take
{
{} };
thus thesis by
Def3,
INSTALG1: 15;
end;
thus thesis;
end;
end
definition
mode
CatSignature is
Categorial
Signature;
end
definition
let A be
set;
::
CATALG_1:def5
mode
CatSignature of A ->
Signature means
:
Def5: (
CatSign A) is
Subsignature of it & the
carrier of it
=
[:
{
0 }, (2
-tuples_on A):];
existence
proof
set S = (
CatSign A);
S is
Subsignature of S & the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):] by
Def3,
INSTALG1: 15;
then
reconsider S as
CatSignature by
Def4;
take S;
thus thesis by
Def3,
INSTALG1: 15;
end;
end
theorem ::
CATALG_1:4
for A1,A2 be
set, S be
CatSignature of A1 st S is
CatSignature of A2 holds A1
= A2
proof
let A1,A2 be
set, S be
CatSignature of A1;
assume that (
CatSign A2) is
Subsignature of S and
A1: the
carrier of S
=
[:
{
0 }, (2
-tuples_on A2):];
A2:
[:
{
0 }, (2
-tuples_on A1):]
=
[:
{
0 }, (2
-tuples_on A2):] by
A1,
Def5;
then
A3: (2
-tuples_on A1)
c= (2
-tuples_on A2) by
ZFMISC_1: 94;
hereby
let x be
object;
assume x
in A1;
then
<*x, x*>
in (2
-tuples_on A1) by
FINSEQ_2: 137;
then
<*x, x*>
in (2
-tuples_on A2) by
A3;
hence x
in A2 by
FINSEQ_2: 138;
end;
let x be
object;
assume x
in A2;
then
A4:
<*x, x*>
in (2
-tuples_on A2) by
FINSEQ_2: 137;
(2
-tuples_on A2)
c= (2
-tuples_on A1) by
A2,
ZFMISC_1: 94;
hence thesis by
A4,
FINSEQ_2: 138;
end;
registration
let A be
set;
cluster ->
Categorial for
CatSignature of A;
coherence
proof
let S be
CatSignature of A;
take A;
thus thesis by
Def5;
end;
end
registration
let A be non
empty
set;
cluster -> non
empty for
CatSignature of A;
coherence
proof
let S be
CatSignature of A;
(
CatSign A) is
Subsignature of S by
Def5;
then the
carrier of (
CatSign A)
c= the
carrier of S by
INSTALG1: 10;
hence not the
carrier of S is
empty;
end;
end
registration
let A be
set;
cluster
strict for
CatSignature of A;
existence
proof
set S = (
CatSign A);
S is
Subsignature of S & the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):] by
Def3,
INSTALG1: 15;
then S is
CatSignature of A by
Def5;
hence thesis;
end;
end
definition
let A be
set;
:: original:
CatSign
redefine
func
CatSign A ->
strict
CatSignature of A ;
coherence
proof
set S = (
CatSign A);
S is
Subsignature of S & the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):] by
Def3,
INSTALG1: 15;
hence thesis by
Def5;
end;
end
definition
let S be
ManySortedSign;
assume
A1: for x be
object st x
in (
proj2 (the
carrier of S
\/ the
carrier' of S)) holds x is
Function;
::
CATALG_1:def6
func
underlay S ->
set means
:
Def6: for x be
object holds x
in it iff ex a be
set, f be
Function st
[a, f]
in (the
carrier of S
\/ the
carrier' of S) & x
in (
rng f);
existence
proof
set A = (the
carrier of S
\/ the
carrier' of S);
take X = (
proj2 (
union (
proj2 A)));
let x be
object;
hereby
assume x
in X;
then
consider a be
object such that
A2:
[a, x]
in (
union (
proj2 A)) by
XTUPLE_0:def 13;
consider b be
set such that
A3:
[a, x]
in b and
A4: b
in (
proj2 A) by
A2,
TARSKI:def 4;
reconsider b as
Function by
A4,
A1;
b
in (
proj2 A) by
A4;
then
consider c be
object such that
A5:
[c, b]
in A by
XTUPLE_0:def 13;
reconsider c as
set by
TARSKI: 1;
take c, b;
thus
[c, b]
in A & x
in (
rng b) by
A3,
A5,
XTUPLE_0:def 13;
end;
given a be
set, f be
Function such that
A6:
[a, f]
in (the
carrier of S
\/ the
carrier' of S) and
A7: x
in (
rng f);
consider b be
object such that
A8:
[b, x]
in f by
A7,
XTUPLE_0:def 13;
f
in (
proj2 A) by
A6,
XTUPLE_0:def 13;
then f
in (
proj2 A);
then
[b, x]
in (
union (
proj2 A)) by
A8,
TARSKI:def 4;
hence thesis by
XTUPLE_0:def 13;
end;
uniqueness
proof
defpred
P[
object] means ex a be
set, f be
Function st
[a, f]
in (the
carrier of S
\/ the
carrier' of S) & $1
in (
rng f);
thus for X1,X2 be
set st (for x be
object holds x
in X1 iff
P[x]) & (for x be
object holds x
in X2 iff
P[x]) holds X1
= X2 from
XBOOLE_0:sch 3;
end;
end
definition
let S be
ManySortedSign;
::
CATALG_1:def7
attr S is
delta-concrete means
:
Def7: ex f be
sequence of
NAT st (for s be
object st s
in the
carrier of S holds ex i be
Element of
NAT , p be
FinSequence st s
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier of S) & (for o be
object st o
in the
carrier' of S holds ex i be
Element of
NAT , p be
FinSequence st o
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier' of S);
end
Lm2: for A be
set, x be
object st x
in (
proj2 (the
carrier of (
CatSign A)
\/ the
carrier' of (
CatSign A))) holds x is
Function
proof
let A be
set, x be
object;
set C1 = the
carrier of (
CatSign A), C2 = the
carrier' of (
CatSign A);
A1: C1
=
[:
{
0 }, (2
-tuples_on A):] by
Def3;
A2: C2
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
Def3;
assume x
in (
proj2 (C1
\/ C2));
then x
in ((
proj2 C1)
\/ (
proj2 C2)) by
XTUPLE_0: 27;
per cases by
XBOOLE_0:def 3;
suppose x
in (
proj2 C1);
then x
in (2
-tuples_on A) by
A1,
FUNCT_5: 9;
hence x is
Function;
end;
suppose x
in (
proj2 C2);
then x
in ((
proj2
[:
{1}, (1
-tuples_on A):])
\/ (
proj2
[:
{2}, (3
-tuples_on A):])) by
A2,
XTUPLE_0: 27;
per cases by
XBOOLE_0:def 3;
suppose x
in (
proj2
[:
{1}, (1
-tuples_on A):]);
then x
in (1
-tuples_on A) by
FUNCT_5: 9;
hence x is
Function;
end;
suppose x
in (
proj2
[:
{2}, (3
-tuples_on A):]);
then x
in (3
-tuples_on A) by
FUNCT_5: 9;
hence x is
Function;
end;
end;
end;
theorem ::
CATALG_1:5
Th5: for A be
set holds (
underlay (
CatSign A))
= A
proof
let A be
set;
set S = (
CatSign A);
A1: the
carrier' of S
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
Def3;
A2: for x be
object st x
in (
proj2 (the
carrier of (
CatSign A)
\/ the
carrier' of (
CatSign A))) holds x is
Function by
Lm2;
hereby
let x be
object;
assume x
in (
underlay (
CatSign A));
then
consider a be
set, f be
Function such that
A3:
[a, f]
in (the
carrier of S
\/ the
carrier' of S) and
A4: x
in (
rng f) by
Def6,
A2;
[a, f]
in the
carrier of S or
[a, f]
in the
carrier' of S by
A3,
XBOOLE_0:def 3;
then
[a, f]
in
[:
{
0 }, (2
-tuples_on A):] or
[a, f]
in
[:
{1}, (1
-tuples_on A):] or
[a, f]
in
[:
{2}, (3
-tuples_on A):] by
A1,
Def3,
XBOOLE_0:def 3;
then f
in (2
-tuples_on A) or f
in (1
-tuples_on A) or f
in (3
-tuples_on A) by
ZFMISC_1: 87;
then f is
FinSequence of A by
FINSEQ_2:def 3;
then (
rng f)
c= A by
FINSEQ_1:def 4;
hence x
in A by
A4;
end;
let x be
object;
assume x
in A;
then
A5:
<*x, x*>
in (2
-tuples_on A) by
FINSEQ_2: 137;
the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):] by
Def3;
then
[
0 ,
<*x, x*>]
in the
carrier of S by
A5,
ZFMISC_1: 105;
then
A6:
[
0 ,
<*x, x*>]
in (the
carrier of S
\/ the
carrier' of S) by
XBOOLE_0:def 3;
(
rng
<*x, x*>)
=
{x, x} by
FINSEQ_2: 127;
then x
in (
rng
<*x, x*>) by
TARSKI:def 2;
hence thesis by
A6,
Def6,
A2;
end;
registration
let A be
set;
cluster (
CatSign A) ->
delta-concrete;
coherence
proof
defpred
P[
object,
object] means ($1
=
0 implies $2
= 2) & ($1
= 1 implies $2
= 1) & ($1
= 2 implies $2
= 3);
set S = (
CatSign A);
A1: for x be
object st x
in
NAT holds ex y be
object st y
in
NAT &
P[x, y]
proof
reconsider j0 = 2, j1 = 1, j2 = 3 as
set;
let i be
object;
assume i
in
NAT ;
per cases ;
suppose
A2: i
=
0 ;
take j0;
thus thesis by
A2;
end;
suppose
A3: i
= 1;
take j1;
thus thesis by
A3;
end;
suppose
A4: i
= 2;
take j2;
thus thesis by
A4;
end;
suppose
A5: i
<>
0 & i
<> 1 & i
<> 2;
take j0;
thus thesis by
A5;
end;
end;
consider f be
Function such that
A6: (
dom f)
=
NAT & (
rng f)
c=
NAT and
A7: for i be
object st i
in
NAT holds
P[i, (f
. i)] from
FUNCT_1:sch 6(
A1);
reconsider f as
sequence of
NAT by
A6,
FUNCT_2: 2;
take f;
A8: A
= (
underlay S) by
Th5;
A9: the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):] by
Def3;
hereby
let s be
object;
assume s
in the
carrier of S;
then
consider i,p be
object such that
A10: i
in
{
0 } and
A11: p
in (2
-tuples_on A) and
A12: s
=
[i, p] by
A9,
ZFMISC_1: 84;
reconsider p as
FinSequence by
A11;
take i =
0 , p;
(f
. i)
= 2 by
A7;
hence s
=
[i, p] & (
len p)
= (f
. i) by
A10,
A11,
A12,
FINSEQ_2: 132,
TARSKI:def 1;
thus
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier of S by
A7,
A9,
A8;
end;
let o be
object;
A13: the
carrier' of S
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
Def3;
assume
A14: o
in the
carrier' of S;
per cases by
A13,
A14,
XBOOLE_0:def 3;
suppose o
in
[:
{1}, (1
-tuples_on A):];
then
consider i,p be
object such that
A15: i
in
{1} and
A16: p
in (1
-tuples_on A) and
A17: o
=
[i, p] by
ZFMISC_1: 84;
reconsider p as
FinSequence of A by
A16,
FINSEQ_2:def 3;
take i = 1, p;
(f
. i)
= 1 by
A7;
hence thesis by
A13,
A8,
A15,
A16,
A17,
FINSEQ_2: 132,
TARSKI:def 1,
XBOOLE_1: 7;
end;
suppose o
in
[:
{2}, (3
-tuples_on A):];
then
consider i,p be
object such that
A18: i
in
{2} and
A19: p
in (3
-tuples_on A) and
A20: o
=
[i, p] by
ZFMISC_1: 84;
reconsider p as
FinSequence of A by
A19,
FINSEQ_2:def 3;
take i = 2, p;
(f
. i)
= 3 by
A7;
hence thesis by
A13,
A8,
A18,
A19,
A20,
FINSEQ_2: 132,
TARSKI:def 1,
XBOOLE_1: 7;
end;
end;
end
registration
cluster
delta-concrete non
empty
strict for
CatSignature;
existence
proof
take (
CatSign
{
{} });
thus thesis;
end;
let A be
set;
cluster
delta-concrete
strict for
CatSignature of A;
existence
proof
take (
CatSign A);
thus thesis;
end;
end
theorem ::
CATALG_1:6
for A be
set holds (
underlay (
CatSign A))
= A
proof
let A be
set;
set S = (
CatSign A);
A1: the
carrier' of S
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
Def3;
A2: for x be
object st x
in (
proj2 (the
carrier of (
CatSign A)
\/ the
carrier' of (
CatSign A))) holds x is
Function by
Lm2;
hereby
let x be
object;
assume x
in (
underlay (
CatSign A));
then
consider a be
set, f be
Function such that
A3:
[a, f]
in (the
carrier of S
\/ the
carrier' of S) and
A4: x
in (
rng f) by
Def6,
A2;
[a, f]
in the
carrier of S or
[a, f]
in the
carrier' of S by
A3,
XBOOLE_0:def 3;
then
[a, f]
in
[:
{
0 }, (2
-tuples_on A):] or
[a, f]
in
[:
{1}, (1
-tuples_on A):] or
[a, f]
in
[:
{2}, (3
-tuples_on A):] by
A1,
Def3,
XBOOLE_0:def 3;
then f
in (2
-tuples_on A) or f
in (1
-tuples_on A) or f
in (3
-tuples_on A) by
ZFMISC_1: 87;
then f is
FinSequence of A by
FINSEQ_2:def 3;
then (
rng f)
c= A by
FINSEQ_1:def 4;
hence x
in A by
A4;
end;
let x be
object;
assume x
in A;
then
A5:
<*x, x*>
in (2
-tuples_on A) by
FINSEQ_2: 137;
the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):] by
Def3;
then
[
0 ,
<*x, x*>]
in the
carrier of S by
A5,
ZFMISC_1: 105;
then
A6:
[
0 ,
<*x, x*>]
in (the
carrier of S
\/ the
carrier' of S) by
XBOOLE_0:def 3;
(
rng
<*x, x*>)
=
{x, x} by
FINSEQ_2: 127;
then x
in (
rng
<*x, x*>) by
TARSKI:def 2;
hence thesis by
A6,
Def6,
A2;
end;
registration
let A be
set;
cluster (
CatSign A) ->
delta-concrete;
coherence ;
end
registration
cluster
delta-concrete non
empty
strict for
CatSignature;
existence
proof
take (
CatSign
{
{} });
thus thesis;
end;
let A be
set;
cluster
delta-concrete
strict for
CatSignature of A;
existence
proof
take (
CatSign A);
thus thesis;
end;
end
Lm3: for S be
delta-concrete
ManySortedSign, x be
object st x
in (
proj2 (the
carrier of S
\/ the
carrier' of S)) holds x is
Function
proof
let S be
delta-concrete
ManySortedSign, x be
object;
consider f be
sequence of
NAT such that
A1: for s be
object st s
in the
carrier of S holds ex i be
Element of
NAT , p be
FinSequence st s
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier of S and
A2: for o be
object st o
in the
carrier' of S holds ex i be
Element of
NAT , p be
FinSequence st o
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier' of S by
Def7;
set C1 = the
carrier of S, C2 = the
carrier' of S;
assume x
in (
proj2 (the
carrier of S
\/ the
carrier' of S));
then
consider y be
object such that
A3:
[y, x]
in (the
carrier of S
\/ the
carrier' of S) by
XTUPLE_0:def 13;
per cases by
XBOOLE_0:def 3,
A3;
suppose
[y, x]
in C1;
then
consider i be
Element of
NAT , p be
FinSequence such that
A4:
[y, x]
=
[i, p] and (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier of S by
A1;
x
= p by
A4,
XTUPLE_0: 1;
hence x is
Function;
end;
suppose
[y, x]
in C2;
then
consider i be
Element of
NAT , p be
FinSequence such that
A5:
[y, x]
=
[i, p] and (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier' of S by
A2;
x
= p by
A5,
XTUPLE_0: 1;
hence x is
Function;
end;
end;
theorem ::
CATALG_1:7
Th7: for S be
delta-concrete
ManySortedSign, x be
set st x
in the
carrier of S or x
in the
carrier' of S holds ex i be
Element of
NAT , p be
FinSequence st x
=
[i, p] & (
rng p)
c= (
underlay S)
proof
let S be
delta-concrete
ManySortedSign, x be
set such that
A1: x
in the
carrier of S or x
in the
carrier' of S;
A2: x
in (the
carrier of S
\/ the
carrier' of S) by
A1,
XBOOLE_0:def 3;
consider f be
sequence of
NAT such that
A3: for s be
object st s
in the
carrier of S holds ex i be
Element of
NAT , p be
FinSequence st s
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier of S and
A4: for o be
object st o
in the
carrier' of S holds ex i be
Element of
NAT , p be
FinSequence st o
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier' of S by
Def7;
A5: for x be
object st x
in (
proj2 (the
carrier of S
\/ the
carrier' of S)) holds x is
Function by
Lm3;
per cases by
A1;
suppose x
in the
carrier of S;
then
consider i be
Element of
NAT , p be
FinSequence such that
A6: x
=
[i, p] and (
len p)
= (f
. i) and
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier of S by
A3;
take i, p;
thus x
=
[i, p] by
A6;
let a be
object;
thus thesis by
A2,
A6,
Def6,
A5;
end;
suppose x
in the
carrier' of S;
then
consider i be
Element of
NAT , p be
FinSequence such that
A7: x
=
[i, p] and (
len p)
= (f
. i) and
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier' of S by
A4;
take i, p;
thus x
=
[i, p] by
A7;
let a be
object;
thus thesis by
A2,
A7,
Def6,
A5;
end;
end;
theorem ::
CATALG_1:8
for S be
delta-concrete
ManySortedSign, i be
set, p1,p2 be
FinSequence st
[i, p1]
in the
carrier of S &
[i, p2]
in the
carrier of S or
[i, p1]
in the
carrier' of S &
[i, p2]
in the
carrier' of S holds (
len p1)
= (
len p2)
proof
let S be
delta-concrete
ManySortedSign, i be
set, p1,p2 be
FinSequence such that
A1:
[i, p1]
in the
carrier of S &
[i, p2]
in the
carrier of S or
[i, p1]
in the
carrier' of S &
[i, p2]
in the
carrier' of S;
consider f be
sequence of
NAT such that
A2: for s be
object st s
in the
carrier of S holds ex i be
Element of
NAT , p be
FinSequence st s
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier of S and
A3: for o be
object st o
in the
carrier' of S holds ex i be
Element of
NAT , p be
FinSequence st o
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier' of S by
Def7;
per cases by
A1;
suppose
A4:
[i, p1]
in the
carrier of S &
[i, p2]
in the
carrier of S;
then
consider j1 be
Element of
NAT , q1 be
FinSequence such that
A5:
[i, p1]
=
[j1, q1] and
A6: (
len q1)
= (f
. j1) and
[:
{j1}, ((f
. j1)
-tuples_on (
underlay S)):]
c= the
carrier of S by
A2;
A7: i
= j1 & p1
= q1 by
A5,
XTUPLE_0: 1;
consider j2 be
Element of
NAT , q2 be
FinSequence such that
A8:
[i, p2]
=
[j2, q2] and
A9: (
len q2)
= (f
. j2) and
[:
{j2}, ((f
. j2)
-tuples_on (
underlay S)):]
c= the
carrier of S by
A2,
A4;
i
= j2 by
A8,
XTUPLE_0: 1;
hence thesis by
A6,
A8,
A9,
A7,
XTUPLE_0: 1;
end;
suppose
A10:
[i, p1]
in the
carrier' of S &
[i, p2]
in the
carrier' of S;
then
consider j1 be
Element of
NAT , q1 be
FinSequence such that
A11:
[i, p1]
=
[j1, q1] and
A12: (
len q1)
= (f
. j1) and
[:
{j1}, ((f
. j1)
-tuples_on (
underlay S)):]
c= the
carrier' of S by
A3;
A13: i
= j1 & p1
= q1 by
A11,
XTUPLE_0: 1;
consider j2 be
Element of
NAT , q2 be
FinSequence such that
A14:
[i, p2]
=
[j2, q2] and
A15: (
len q2)
= (f
. j2) and
[:
{j2}, ((f
. j2)
-tuples_on (
underlay S)):]
c= the
carrier' of S by
A3,
A10;
i
= j2 by
A14,
XTUPLE_0: 1;
hence thesis by
A12,
A14,
A15,
A13,
XTUPLE_0: 1;
end;
end;
theorem ::
CATALG_1:9
for S be
delta-concrete
ManySortedSign, i be
set, p1,p2 be
FinSequence st (
len p2)
= (
len p1) & (
rng p2)
c= (
underlay S) holds (
[i, p1]
in the
carrier of S implies
[i, p2]
in the
carrier of S) & (
[i, p1]
in the
carrier' of S implies
[i, p2]
in the
carrier' of S)
proof
let S be
delta-concrete
ManySortedSign, i be
set, p1,p2 be
FinSequence such that
A1: (
len p2)
= (
len p1) & (
rng p2)
c= (
underlay S);
consider f be
sequence of
NAT such that
A2: for s be
object st s
in the
carrier of S holds ex i be
Element of
NAT , p be
FinSequence st s
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier of S and
A3: for o be
object st o
in the
carrier' of S holds ex i be
Element of
NAT , p be
FinSequence st o
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier' of S by
Def7;
hereby
assume
[i, p1]
in the
carrier of S;
then
consider j1 be
Element of
NAT , q1 be
FinSequence such that
A4:
[i, p1]
=
[j1, q1] and
A5: (
len q1)
= (f
. j1) and
A6:
[:
{j1}, ((f
. j1)
-tuples_on (
underlay S)):]
c= the
carrier of S by
A2;
p1
= q1 by
A4,
XTUPLE_0: 1;
then
A7: p2
in ((f
. j1)
-tuples_on (
underlay S)) by
A1,
A5,
FINSEQ_2: 132;
i
= j1 by
A4,
XTUPLE_0: 1;
then
[i, p2]
in
[:
{j1}, ((f
. j1)
-tuples_on (
underlay S)):] by
A7,
ZFMISC_1: 105;
hence
[i, p2]
in the
carrier of S by
A6;
end;
assume
[i, p1]
in the
carrier' of S;
then
consider j1 be
Element of
NAT , q1 be
FinSequence such that
A8:
[i, p1]
=
[j1, q1] and
A9: (
len q1)
= (f
. j1) and
A10:
[:
{j1}, ((f
. j1)
-tuples_on (
underlay S)):]
c= the
carrier' of S by
A3;
p1
= q1 by
A8,
XTUPLE_0: 1;
then
A11: p2
in ((f
. j1)
-tuples_on (
underlay S)) by
A1,
A9,
FINSEQ_2: 132;
i
= j1 by
A8,
XTUPLE_0: 1;
then
[i, p2]
in
[:
{j1}, ((f
. j1)
-tuples_on (
underlay S)):] by
A11,
ZFMISC_1: 105;
hence thesis by
A10;
end;
theorem ::
CATALG_1:10
for S be
delta-concrete
Categorial non
empty
Signature holds S is
CatSignature of (
underlay S)
proof
let S be
delta-concrete
Categorial non
empty
Signature;
set s = the
SortSymbol of S;
consider A be
set such that
A1: (
CatSign A) is
Subsignature of S and
A2: the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):] by
Def4;
consider f be
sequence of
NAT such that
A3: for s be
object st s
in the
carrier of S holds ex i be
Element of
NAT , p be
FinSequence st s
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier of S and for o be
object st o
in the
carrier' of S holds ex i be
Element of
NAT , p be
FinSequence st o
=
[i, p] & (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier' of S by
Def7;
consider i be
Element of
NAT , p be
FinSequence such that
A4: s
=
[i, p] and
A5: (
len p)
= (f
. i) &
[:
{i}, ((f
. i)
-tuples_on (
underlay S)):]
c= the
carrier of S by
A3;
p
in (2
-tuples_on A) by
A2,
A4,
ZFMISC_1: 105;
then
A6: (
len p)
= 2 by
FINSEQ_2: 132;
A7: for x be
object st x
in (
proj2 (the
carrier of S
\/ the
carrier' of S)) holds x is
Function by
Lm3;
A8: A
c= (
underlay S)
proof
let x be
object;
assume x
in A;
then
<*x, x*>
in (2
-tuples_on A) by
FINSEQ_2: 137;
then
[
0 ,
<*x, x*>]
in the
carrier of S by
A2,
ZFMISC_1: 105;
then
A9:
[
0 ,
<*x, x*>]
in (the
carrier of S
\/ the
carrier' of S) by
XBOOLE_0:def 3;
(
rng
<*x, x*>)
=
{x, x} by
FINSEQ_2: 127;
then x
in (
rng
<*x, x*>) by
TARSKI:def 2;
hence thesis by
A9,
Def6,
A7;
end;
i
=
0 by
A2,
A4,
ZFMISC_1: 105;
then
A10: (2
-tuples_on (
underlay S))
c= (2
-tuples_on A) by
A2,
A5,
A6,
ZFMISC_1: 94;
(
underlay S)
c= A
proof
let x be
object;
assume x
in (
underlay S);
then
<*x, x*>
in (2
-tuples_on (
underlay S)) by
FINSEQ_2: 137;
hence thesis by
A10,
FINSEQ_2: 138;
end;
then A
= (
underlay S) by
A8;
hence thesis by
A1,
A2,
Def5;
end;
begin
registration
let S be non
empty
CatSignature;
let s be
SortSymbol of S;
cluster (s
`2 ) ->
Relation-like
Function-like;
coherence
proof
consider A be
set such that (
CatSign A) is
Subsignature of S and
A1: the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):] by
Def4;
(s
`2 )
in (2
-tuples_on A) by
A1,
MCART_1: 10;
hence thesis;
end;
end
registration
let S be non
empty
delta-concrete
ManySortedSign;
let s be
SortSymbol of S;
cluster (s
`2 ) ->
Relation-like
Function-like;
coherence
proof
ex i be
Element of
NAT , p be
FinSequence st (s
=
[i, p]) & ((
rng p)
c= (
underlay S)) by
Th7;
hence thesis;
end;
end
registration
let S be non
void
delta-concrete
ManySortedSign;
let o be
Element of the
carrier' of S;
cluster (o
`2 ) ->
Relation-like
Function-like;
coherence
proof
ex i be
Element of
NAT , p be
FinSequence st (o
=
[i, p]) & ((
rng p)
c= (
underlay S)) by
Th7;
hence thesis;
end;
end
registration
let S be non
empty
CatSignature;
let s be
SortSymbol of S;
cluster (s
`2 ) ->
FinSequence-like;
coherence
proof
consider A be
set such that (
CatSign A) is
Subsignature of S and
A1: the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):] by
Def4;
(s
`2 )
in (2
-tuples_on A) by
A1,
MCART_1: 10;
then ex a,b be
object st a
in A & b
in A & (s
`2 )
=
<*a, b*> by
FINSEQ_2: 137;
hence thesis;
end;
end
registration
let S be non
empty
delta-concrete
ManySortedSign;
let s be
SortSymbol of S;
cluster (s
`2 ) ->
FinSequence-like;
coherence
proof
ex i be
Element of
NAT , p be
FinSequence st (s
=
[i, p]) & ((
rng p)
c= (
underlay S)) by
Th7;
hence thesis;
end;
end
registration
let S be non
void
delta-concrete
ManySortedSign;
let o be
Element of the
carrier' of S;
cluster (o
`2 ) ->
FinSequence-like;
coherence
proof
ex i be
Element of
NAT , p be
FinSequence st (o
=
[i, p]) & ((
rng p)
c= (
underlay S)) by
Th7;
hence thesis;
end;
end
definition
let a be
set;
::
CATALG_1:def8
func
idsym a ->
set equals
[1,
<*a*>];
correctness ;
let b be
set;
::
CATALG_1:def9
func
homsym (a,b) ->
set equals
[
0 ,
<*a, b*>];
correctness ;
let c be
set;
::
CATALG_1:def10
func
compsym (a,b,c) ->
set equals
[2,
<*a, b, c*>];
correctness ;
end
theorem ::
CATALG_1:11
Th11: for A be non
empty
set, S be
CatSignature of A holds for a be
Element of A holds (
idsym a)
in the
carrier' of S & for b be
Element of A holds (
homsym (a,b))
in the
carrier of S & for c be
Element of A holds (
compsym (a,b,c))
in the
carrier' of S
proof
let A be non
empty
set, S be
CatSignature of A;
let a be
Element of A;
A1: the
carrier' of (
CatSign A)
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
Def3;
A2: (
CatSign A) is
Subsignature of S by
Def5;
then
A3: the
carrier of (
CatSign A)
c= the
carrier of S by
INSTALG1: 10;
A4: the
carrier' of (
CatSign A)
c= the
carrier' of S by
A2,
INSTALG1: 10;
<*a*>
in (1
-tuples_on A) by
FINSEQ_2: 135;
then
[1,
<*a*>]
in
[:
{1}, (1
-tuples_on A):] by
ZFMISC_1: 105;
then
[1,
<*a*>]
in the
carrier' of (
CatSign A) by
A1,
XBOOLE_0:def 3;
hence (
idsym a)
in the
carrier' of S by
A4;
let b be
Element of A;
A5: the
carrier of (
CatSign A)
=
[:
{
0 }, (2
-tuples_on A):] by
Def3;
<*a, b*>
in (2
-tuples_on A) by
FINSEQ_2: 137;
then
[
0 ,
<*a, b*>]
in
[:
{
0 }, (2
-tuples_on A):] by
ZFMISC_1: 105;
hence (
homsym (a,b))
in the
carrier of S by
A3,
A5;
let c be
Element of A;
<*a, b, c*>
in (3
-tuples_on A) by
FINSEQ_2: 139;
then
[2,
<*a, b, c*>]
in
[:
{2}, (3
-tuples_on A):] by
ZFMISC_1: 105;
then
[2,
<*a, b, c*>]
in the
carrier' of (
CatSign A) by
A1,
XBOOLE_0:def 3;
hence thesis by
A4;
end;
definition
let A be non
empty
set;
let a be
Element of A;
:: original:
idsym
redefine
func
idsym a ->
OperSymbol of (
CatSign A) ;
correctness by
Th11;
let b be
Element of A;
:: original:
homsym
redefine
func
homsym (a,b) ->
SortSymbol of (
CatSign A) ;
correctness by
Th11;
let c be
Element of A;
:: original:
compsym
redefine
func
compsym (a,b,c) ->
OperSymbol of (
CatSign A) ;
correctness by
Th11;
end
theorem ::
CATALG_1:12
Th12: for a,b be
set st (
idsym a)
= (
idsym b) holds a
= b
proof
let a,b be
set;
assume (
idsym a)
= (
idsym b);
then
<*a*>
=
<*b*> by
XTUPLE_0: 1;
hence thesis by
Lm1;
end;
theorem ::
CATALG_1:13
Th13: for a1,b1,a2,b2 be
set st (
homsym (a1,a2))
= (
homsym (b1,b2)) holds a1
= b1 & a2
= b2
proof
let a1,b1,a2,b2 be
set;
assume (
homsym (a1,a2))
= (
homsym (b1,b2));
then
A1:
<*a1, a2*>
=
<*b1, b2*> by
XTUPLE_0: 1;
(
<*a1, a2*>
. 1)
= a1 & (
<*a1, a2*>
. 2)
= a2 by
FINSEQ_1: 44;
hence thesis by
A1,
FINSEQ_1: 44;
end;
theorem ::
CATALG_1:14
Th14: for a1,b1,a2,b2,a3,b3 be
set st (
compsym (a1,a2,a3))
= (
compsym (b1,b2,b3)) holds a1
= b1 & a2
= b2 & a3
= b3
proof
let a1,b1,a2,b2,a3,b3 be
set;
A1: (
<*a1, a2, a3*>
. 3)
= a3 by
FINSEQ_1: 45;
assume (
compsym (a1,a2,a3))
= (
compsym (b1,b2,b3));
then
A2:
<*a1, a2, a3*>
=
<*b1, b2, b3*> by
XTUPLE_0: 1;
(
<*a1, a2, a3*>
. 1)
= a1 & (
<*a1, a2, a3*>
. 2)
= a2 by
FINSEQ_1: 45;
hence thesis by
A2,
A1,
FINSEQ_1: 45;
end;
theorem ::
CATALG_1:15
Th15: for A be non
empty
set, S be
CatSignature of A holds for s be
SortSymbol of S holds ex a,b be
Element of A st s
= (
homsym (a,b))
proof
let A be non
empty
set, S be
CatSignature of A;
let s be
SortSymbol of S;
A1: the
carrier of S
=
[:
{
0 }, (2
-tuples_on A):] by
Def5;
then (s
`2 )
in (2
-tuples_on A) by
MCART_1: 10;
then (s
`2 )
in { z where z be
Element of (A
* ) : (
len z)
= 2 } by
FINSEQ_2:def 4;
then
consider z be
Element of (A
* ) such that
A2: (s
`2 )
= z and
A3: (
len z)
= 2;
A4: (z
. 1)
in
{(z
. 1), (z
. 2)} & (z
. 2)
in
{(z
. 1), (z
. 2)} by
TARSKI:def 2;
A5: z
=
<*(z
. 1), (z
. 2)*> by
A3,
FINSEQ_1: 44;
then (
rng z)
=
{(z
. 1), (z
. 2)} by
FINSEQ_2: 127;
then
reconsider a = (z
. 1), b = (z
. 2) as
Element of A by
A4;
take a, b;
s
=
[(s
`1 ), (s
`2 )] & (s
`1 )
in
{
0 } by
A1,
MCART_1: 10,
MCART_1: 21;
hence thesis by
A2,
A5,
TARSKI:def 1;
end;
theorem ::
CATALG_1:16
Th16: for A be non
empty
set, o be
OperSymbol of (
CatSign A) holds (o
`1 )
= 1 & (
len (o
`2 ))
= 1 or (o
`1 )
= 2 & (
len (o
`2 ))
= 3
proof
let A be non
empty
set, o be
OperSymbol of (
CatSign A);
the
carrier' of (
CatSign A)
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
Def3;
then o
in
[:
{1}, (1
-tuples_on A):] or o
in
[:
{2}, (3
-tuples_on A):] by
XBOOLE_0:def 3;
then (o
`1 )
in
{1} & (o
`2 )
in (1
-tuples_on A) or (o
`1 )
in
{2} & (o
`2 )
in (3
-tuples_on A) by
MCART_1: 10;
hence thesis by
CARD_1:def 7,
TARSKI:def 1;
end;
theorem ::
CATALG_1:17
Th17: for A be non
empty
set, o be
OperSymbol of (
CatSign A) st (o
`1 )
= 1 or (
len (o
`2 ))
= 1 holds ex a be
Element of A st o
= (
idsym a)
proof
let A be non
empty
set, o be
OperSymbol of (
CatSign A) such that
A1: (o
`1 )
= 1 or (
len (o
`2 ))
= 1;
the
carrier' of (
CatSign A)
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
Def3;
then o
in
[:
{1}, (1
-tuples_on A):] or o
in
[:
{2}, (3
-tuples_on A):] by
XBOOLE_0:def 3;
then
A2: (o
`1 )
in
{1} & (o
`2 )
in (1
-tuples_on A) & o
=
[(o
`1 ), (o
`2 )] or (o
`1 )
in
{2} & (o
`2 )
in (3
-tuples_on A) by
MCART_1: 10,
MCART_1: 21;
then
consider a be
set such that
A3: a
in A and
A4: (o
`2 )
=
<*a*> by
A1,
CARD_1:def 7,
FINSEQ_2: 135,
TARSKI:def 1;
reconsider a as
Element of A by
A3;
take a;
thus thesis by
A1,
A2,
A4,
CARD_1:def 7,
TARSKI:def 1;
end;
theorem ::
CATALG_1:18
Th18: for A be non
empty
set, o be
OperSymbol of (
CatSign A) st (o
`1 )
= 2 or (
len (o
`2 ))
= 3 holds ex a,b,c be
Element of A st o
= (
compsym (a,b,c))
proof
let A be non
empty
set, o be
OperSymbol of (
CatSign A) such that
A1: (o
`1 )
= 2 or (
len (o
`2 ))
= 3;
the
carrier' of (
CatSign A)
= (
[:
{1}, (1
-tuples_on A):]
\/
[:
{2}, (3
-tuples_on A):]) by
Def3;
then o
in
[:
{1}, (1
-tuples_on A):] or o
in
[:
{2}, (3
-tuples_on A):] by
XBOOLE_0:def 3;
then
A2: (o
`1 )
in
{1} & (o
`2 )
in (1
-tuples_on A) or (o
`1 )
in
{2} & (o
`2 )
in (3
-tuples_on A) & o
=
[(o
`1 ), (o
`2 )] by
MCART_1: 10,
MCART_1: 21;
then
consider a,b,c be
object such that
A3: a
in A & b
in A & c
in A and
A4: (o
`2 )
=
<*a, b, c*> by
A1,
CARD_1:def 7,
FINSEQ_2: 139,
TARSKI:def 1;
reconsider a, b, c as
Element of A by
A3;
take a, b, c;
thus thesis by
A1,
A2,
A4,
CARD_1:def 7,
TARSKI:def 1;
end;
theorem ::
CATALG_1:19
for A be non
empty
set, a be
Element of A holds (
the_arity_of (
idsym a))
=
{} & (
the_result_sort_of (
idsym a))
= (
homsym (a,a)) by
Def3;
theorem ::
CATALG_1:20
for A be non
empty
set, a,b,c be
Element of A holds (
the_arity_of (
compsym (a,b,c)))
=
<*(
homsym (b,c)), (
homsym (a,b))*> & (
the_result_sort_of (
compsym (a,b,c)))
= (
homsym (a,c)) by
Def3;
begin
definition
let C1,C2 be
Category;
let F be
Functor of C1, C2;
::
CATALG_1:def11
func
Upsilon F ->
Function of the
carrier of (
CatSign the
carrier of C1), the
carrier of (
CatSign the
carrier of C2) means
:
Def11: for s be
SortSymbol of (
CatSign the
carrier of C1) holds (it
. s)
=
[
0 , ((
Obj F)
* (s
`2 ))];
uniqueness
proof
let U1,U2 be
Function of the
carrier of (
CatSign the
carrier of C1), the
carrier of (
CatSign the
carrier of C2) such that
A1: for s be
SortSymbol of (
CatSign the
carrier of C1) holds (U1
. s)
=
[
0 , ((
Obj F)
* (s
`2 ))] and
A2: for s be
SortSymbol of (
CatSign the
carrier of C1) holds (U2
. s)
=
[
0 , ((
Obj F)
* (s
`2 ))];
now
let s be
SortSymbol of (
CatSign the
carrier of C1);
thus (U1
. s)
=
[
0 , ((
Obj F)
* (s
`2 ))] by
A1
.= (U2
. s) by
A2;
end;
hence thesis;
end;
existence
proof
deffunc
f(
SortSymbol of (
CatSign the
carrier of C1)) =
[
0 , ((
Obj F)
* ($1
`2 ))];
consider Up be
Function such that
A3: (
dom Up)
= the
carrier of (
CatSign the
carrier of C1) and
A4: for s be
SortSymbol of (
CatSign the
carrier of C1) holds (Up
. s)
=
f(s) from
FUNCT_1:sch 4;
(
rng Up)
c= the
carrier of (
CatSign the
carrier of C2)
proof
let x be
object;
assume x
in (
rng Up);
then
consider a be
object such that
A5: a
in (
dom Up) and
A6: x
= (Up
. a) by
FUNCT_1:def 3;
reconsider a as
SortSymbol of (
CatSign the
carrier of C1) by
A3,
A5;
the
carrier of (
CatSign the
carrier of C1)
=
[:
{
0 }, (2
-tuples_on the
carrier of C1):] by
Def3;
then (a
`2 )
in (2
-tuples_on the
carrier of C1) by
MCART_1: 12;
then
consider a1,a2 be
object such that
A7: a1
in the
carrier of C1 & a2
in the
carrier of C1 and
A8: (a
`2 )
=
<*a1, a2*> by
FINSEQ_2: 137;
reconsider a1, a2 as
Object of C1 by
A7;
(
rng
<*a1, a2*>)
c= the
carrier of C1 & (
dom (
Obj F))
= the
carrier of C1 by
FUNCT_2:def 1;
then
A9: (
dom ((
Obj F)
*
<*a1, a2*>))
= (
dom
<*a1, a2*>) by
RELAT_1: 27
.= (
Seg 2) by
FINSEQ_1: 89;
then
reconsider p = ((
Obj F)
*
<*a1, a2*>) as
FinSequence by
FINSEQ_1:def 2;
(
<*a1, a2*>
. 1)
= a1 & 1
in
{1, 2} by
FINSEQ_1: 44,
TARSKI:def 2;
then
A10: (p
. 1)
= ((
Obj F)
. a1) by
A9,
FINSEQ_1: 2,
FUNCT_1: 12;
A11: the
carrier of (
CatSign the
carrier of C2)
=
[:
{
0 }, (2
-tuples_on the
carrier of C2):] by
Def3;
(
<*a1, a2*>
. 2)
= a2 & 2
in
{1, 2} by
FINSEQ_1: 44,
TARSKI:def 2;
then
A12: (p
. 2)
= ((
Obj F)
. a2) by
A9,
FINSEQ_1: 2,
FUNCT_1: 12;
(
len p)
= 2 by
A9,
FINSEQ_1:def 3;
then p
=
<*((
Obj F)
. a1), ((
Obj F)
. a2)*> by
A10,
A12,
FINSEQ_1: 44;
then p
in (2
-tuples_on the
carrier of C2) by
FINSEQ_2: 101;
then
[
0 , p]
in the
carrier of (
CatSign the
carrier of C2) by
A11,
ZFMISC_1: 105;
hence thesis by
A4,
A6,
A8;
end;
then Up is
Function of the
carrier of (
CatSign the
carrier of C1), the
carrier of (
CatSign the
carrier of C2) by
A3,
FUNCT_2:def 1,
RELSET_1: 4;
hence thesis by
A4;
end;
::
CATALG_1:def12
func
Psi F ->
Function of the
carrier' of (
CatSign the
carrier of C1), the
carrier' of (
CatSign the
carrier of C2) means
:
Def12: for o be
OperSymbol of (
CatSign the
carrier of C1) holds (it
. o)
=
[(o
`1 ), ((
Obj F)
* (o
`2 ))];
uniqueness
proof
let U1,U2 be
Function of the
carrier' of (
CatSign the
carrier of C1), the
carrier' of (
CatSign the
carrier of C2) such that
A13: for s be
OperSymbol of (
CatSign the
carrier of C1) holds (U1
. s)
=
[(s
`1 ), ((
Obj F)
* (s
`2 ))] and
A14: for s be
OperSymbol of (
CatSign the
carrier of C1) holds (U2
. s)
=
[(s
`1 ), ((
Obj F)
* (s
`2 ))];
now
let s be
OperSymbol of (
CatSign the
carrier of C1);
thus (U1
. s)
=
[(s
`1 ), ((
Obj F)
* (s
`2 ))] by
A13
.= (U2
. s) by
A14;
end;
hence thesis;
end;
existence
proof
deffunc
f(
OperSymbol of (
CatSign the
carrier of C1)) =
[($1
`1 ), ((
Obj F)
* ($1
`2 ))];
consider Up be
Function such that
A15: (
dom Up)
= the
carrier' of (
CatSign the
carrier of C1) and
A16: for s be
OperSymbol of (
CatSign the
carrier of C1) holds (Up
. s)
=
f(s) from
FUNCT_1:sch 4;
(
rng Up)
c= the
carrier' of (
CatSign the
carrier of C2)
proof
let x be
object;
assume x
in (
rng Up);
then
consider a be
object such that
A17: a
in (
dom Up) and
A18: x
= (Up
. a) by
FUNCT_1:def 3;
A19: the
carrier' of (
CatSign the
carrier of C1)
= (
[:
{1}, (1
-tuples_on the
carrier of C1):]
\/
[:
{2}, (3
-tuples_on the
carrier of C1):]) by
Def3;
reconsider a as
OperSymbol of (
CatSign the
carrier of C1) by
A15,
A17;
per cases by
A19,
XBOOLE_0:def 3;
suppose
A20: a
in
[:
{1}, (1
-tuples_on the
carrier of C1):];
then (a
`2 )
in (1
-tuples_on the
carrier of C1) by
MCART_1: 12;
then
consider a1 be
set such that
A21: a1
in the
carrier of C1 and
A22: (a
`2 )
=
<*a1*> by
FINSEQ_2: 135;
reconsider a1 as
Object of C1 by
A21;
(
rng
<*a1*>)
c= the
carrier of C1 & (
dom (
Obj F))
= the
carrier of C1 by
FUNCT_2:def 1;
then
A23: (
dom ((
Obj F)
*
<*a1*>))
= (
dom
<*a1*>) by
RELAT_1: 27
.= (
Seg 1) by
FINSEQ_1: 38;
then
reconsider p = ((
Obj F)
*
<*a1*>) as
FinSequence by
FINSEQ_1:def 2;
A24: (
len p)
= 1 by
A23,
FINSEQ_1:def 3;
(
<*a1*>
. 1)
= a1 & 1
in
{1} by
FINSEQ_1: 40,
TARSKI:def 1;
then (p
. 1)
= ((
Obj F)
. a1) by
A23,
FINSEQ_1: 2,
FUNCT_1: 12;
then p
=
<*((
Obj F)
. a1)*> by
A24,
FINSEQ_1: 40;
then p is
Element of (1
-tuples_on the
carrier of C2) by
FINSEQ_2: 98;
then
A25:
[1, p]
in
[:
{1}, (1
-tuples_on the
carrier of C2):] by
ZFMISC_1: 105;
A26: (a
`1 )
= 1 by
A20,
MCART_1: 12;
the
carrier' of (
CatSign the
carrier of C2)
= (
[:
{1}, (1
-tuples_on the
carrier of C2):]
\/
[:
{2}, (3
-tuples_on the
carrier of C2):]) by
Def3;
then
[1, p]
in the
carrier' of (
CatSign the
carrier of C2) by
A25,
XBOOLE_0:def 3;
hence thesis by
A16,
A18,
A26,
A22;
end;
suppose
A27: a
in
[:
{2}, (3
-tuples_on the
carrier of C1):];
then (a
`2 )
in (3
-tuples_on the
carrier of C1) by
MCART_1: 12;
then
consider a1,a2,a3 be
object such that
A28: a1
in the
carrier of C1 & a2
in the
carrier of C1 & a3
in the
carrier of C1 and
A29: (a
`2 )
=
<*a1, a2, a3*> by
FINSEQ_2: 139;
reconsider a1, a2, a3 as
Object of C1 by
A28;
(
rng
<*a1, a2, a3*>)
c= the
carrier of C1 & (
dom (
Obj F))
= the
carrier of C1 by
FUNCT_2:def 1;
then
A30: (
dom ((
Obj F)
*
<*a1, a2, a3*>))
= (
dom
<*a1, a2, a3*>) by
RELAT_1: 27
.= (
Seg 3) by
FINSEQ_1: 89;
then
reconsider p = ((
Obj F)
*
<*a1, a2, a3*>) as
FinSequence by
FINSEQ_1:def 2;
(
<*a1, a2, a3*>
. 1)
= a1 & 1
in
{1, 2, 3} by
ENUMSET1:def 1,
FINSEQ_1: 45;
then
A31: (p
. 1)
= ((
Obj F)
. a1) by
A30,
FINSEQ_3: 1,
FUNCT_1: 12;
(
<*a1, a2, a3*>
. 3)
= a3 & 3
in
{1, 2, 3} by
ENUMSET1:def 1,
FINSEQ_1: 45;
then
A32: (p
. 3)
= ((
Obj F)
. a3) by
A30,
FINSEQ_3: 1,
FUNCT_1: 12;
(
<*a1, a2, a3*>
. 2)
= a2 & 2
in
{1, 2, 3} by
ENUMSET1:def 1,
FINSEQ_1: 45;
then
A33: (p
. 2)
= ((
Obj F)
. a2) by
A30,
FINSEQ_3: 1,
FUNCT_1: 12;
(
len p)
= 3 by
A30,
FINSEQ_1:def 3;
then p
=
<*((
Obj F)
. a1), ((
Obj F)
. a2), ((
Obj F)
. a3)*> by
A31,
A33,
A32,
FINSEQ_1: 45;
then p is
Element of (3
-tuples_on the
carrier of C2) by
FINSEQ_2: 104;
then
A34:
[2, p]
in
[:
{2}, (3
-tuples_on the
carrier of C2):] by
ZFMISC_1: 105;
A35: (a
`1 )
= 2 by
A27,
MCART_1: 12;
the
carrier' of (
CatSign the
carrier of C2)
= (
[:
{1}, (1
-tuples_on the
carrier of C2):]
\/
[:
{2}, (3
-tuples_on the
carrier of C2):]) by
Def3;
then
[2, p]
in the
carrier' of (
CatSign the
carrier of C2) by
A34,
XBOOLE_0:def 3;
hence thesis by
A16,
A18,
A35,
A29;
end;
end;
then Up is
Function of the
carrier' of (
CatSign the
carrier of C1), the
carrier' of (
CatSign the
carrier of C2) by
A15,
FUNCT_2:def 1,
RELSET_1: 4;
hence thesis by
A16;
end;
end
Lm4:
now
let x be
set, f be
Function;
assume x
in (
dom f);
then (
rng
<*x*>)
=
{x} &
{x}
c= (
dom f) by
FINSEQ_1: 39,
ZFMISC_1: 31;
then
A1: (
dom (f
*
<*x*>))
= (
dom
<*x*>) by
RELAT_1: 27
.= (
Seg 1) by
FINSEQ_1: 38;
then
reconsider p = (f
*
<*x*>) as
FinSequence by
FINSEQ_1:def 2;
A2: (
len p)
= 1 by
A1,
FINSEQ_1:def 3;
1
in
{1} & (
<*x*>
. 1)
= x by
FINSEQ_1: 40,
TARSKI:def 1;
then (p
. 1)
= (f
. x) by
A1,
FINSEQ_1: 2,
FUNCT_1: 12;
hence (f
*
<*x*>)
=
<*(f
. x)*> by
A2,
FINSEQ_1: 40;
end;
theorem ::
CATALG_1:21
Th21: for C1,C2 be
Category, F be
Functor of C1, C2 holds for a,b be
Object of C1 holds ((
Upsilon F)
. (
homsym (a,b)))
= (
homsym ((F
. a),(F
. b)))
proof
let C1,C2 be
Category, F be
Functor of C1, C2;
let a,b be
Object of C1;
A1: (
dom (
Obj F))
= the
carrier of C1 by
FUNCT_2:def 1;
thus ((
Upsilon F)
. (
homsym (a,b)))
=
[
0 , ((
Obj F)
* ((
homsym (a,b))
`2 ))] by
Def11
.=
[
0 , ((
Obj F)
*
<*a, b*>)]
.=
[
0 ,
<*((
Obj F)
. a), ((
Obj F)
. b)*>] by
A1,
FINSEQ_2: 125
.=
[
0 ,
<*(F
. a), ((
Obj F)
. b)*>]
.= (
homsym ((F
. a),(F
. b)));
end;
theorem ::
CATALG_1:22
Th22: for C1,C2 be
Category, F be
Functor of C1, C2 holds for a be
Object of C1 holds ((
Psi F)
. (
idsym a))
= (
idsym (F
. a))
proof
let C1,C2 be
Category, F be
Functor of C1, C2;
let a be
Object of C1;
A1: (
dom (
Obj F))
= the
carrier of C1 by
FUNCT_2:def 1;
((
idsym a)
`1 )
= 1 & ((
idsym a)
`2 )
=
<*a*>;
hence ((
Psi F)
. (
idsym a))
=
[1, ((
Obj F)
*
<*a*>)] by
Def12
.=
[1,
<*((
Obj F)
. a)*>] by
A1,
Lm4
.= (
idsym (F
. a));
end;
theorem ::
CATALG_1:23
Th23: for C1,C2 be
Category, F be
Functor of C1, C2 holds for a,b,c be
Object of C1 holds ((
Psi F)
. (
compsym (a,b,c)))
= (
compsym ((F
. a),(F
. b),(F
. c)))
proof
let C1,C2 be
Category, F be
Functor of C1, C2;
let a,b,c be
Object of C1;
A1: (
dom (
Obj F))
= the
carrier of C1 by
FUNCT_2:def 1;
((
compsym (a,b,c))
`1 )
= 2 & ((
compsym (a,b,c))
`2 )
=
<*a, b, c*>;
hence ((
Psi F)
. (
compsym (a,b,c)))
=
[2, ((
Obj F)
*
<*a, b, c*>)] by
Def12
.=
[2,
<*((
Obj F)
. a), ((
Obj F)
. b), ((
Obj F)
. c)*>] by
A1,
FINSEQ_2: 126
.=
[2,
<*(F
. a), ((
Obj F)
. b), ((
Obj F)
. c)*>]
.=
[2,
<*(F
. a), (F
. b), ((
Obj F)
. c)*>]
.= (
compsym ((F
. a),(F
. b),(F
. c)));
end;
theorem ::
CATALG_1:24
Th24: for C1,C2 be
Category, F be
Functor of C1, C2 holds ((
Upsilon F),(
Psi F))
form_morphism_between ((
CatSign the
carrier of C1),(
CatSign the
carrier of C2))
proof
let C1,C2 be
Category, F be
Functor of C1, C2;
set f = (
Upsilon F), g = (
Psi F);
set S1 = (
CatSign the
carrier of C1), S2 = (
CatSign the
carrier of C2);
thus (
dom f)
= the
carrier of S1 & (
dom g)
= the
carrier' of S1 by
FUNCT_2:def 1;
thus (
rng f)
c= the
carrier of S2 & (
rng g)
c= the
carrier' of S2;
now
let o be
OperSymbol of (
CatSign the
carrier of C1);
per cases by
Th16;
suppose (o
`1 )
= 1;
then
consider a be
Object of C1 such that
A1: o
= (
idsym a) by
Th17;
thus ((f
* the
ResultSort of S1)
. o)
= (f
. (
the_result_sort_of o)) by
FUNCT_2: 15
.= (f
. (
homsym (a,a))) by
A1,
Def3
.= (
homsym ((F
. a),(F
. a))) by
Th21
.= (
the_result_sort_of (
idsym (F
. a))) by
Def3
.= (the
ResultSort of S2
. (g
. (
idsym a))) by
Th22
.= ((the
ResultSort of S2
* g)
. o) by
A1,
FUNCT_2: 15;
end;
suppose (o
`1 )
= 2;
then
consider a,b,c be
Object of C1 such that
A2: o
= (
compsym (a,b,c)) by
Th18;
thus ((f
* the
ResultSort of S1)
. o)
= (f
. (
the_result_sort_of o)) by
FUNCT_2: 15
.= (f
. (
homsym (a,c))) by
A2,
Def3
.= (
homsym ((F
. a),(F
. c))) by
Th21
.= (
the_result_sort_of (
compsym ((F
. a),(F
. b),(F
. c)))) by
Def3
.= (the
ResultSort of S2
. (g
. (
compsym (a,b,c)))) by
Th23
.= ((the
ResultSort of S2
* g)
. o) by
A2,
FUNCT_2: 15;
end;
end;
hence (f
* the
ResultSort of S1)
= (the
ResultSort of S2
* g);
let o be
set, p be
Function;
assume o
in the
carrier' of S1;
then
reconsider o9 = o as
OperSymbol of S1;
assume
A3: p
= (the
Arity of S1
. o);
per cases by
Th16;
suppose (o9
`1 )
= 1;
then
consider a be
Object of C1 such that
A4: o
= (
idsym a) by
Th17;
A5: (f
*
{} )
=
{} ;
p
=
{} by
A3,
A4,
Def3;
hence (f
* p)
= (
the_arity_of (
idsym (F
. a))) by
A5,
Def3
.= (the
Arity of S2
. (g
. o)) by
A4,
Th22;
end;
suppose (o9
`1 )
= 2;
then
consider a,b,c be
Object of C1 such that
A6: o
= (
compsym (a,b,c)) by
Th18;
(
dom f)
= the
carrier of S1 & p
=
<*(
homsym (b,c)), (
homsym (a,b))*> by
A3,
A6,
Def3,
FUNCT_2:def 1;
hence (f
* p)
=
<*(f
. (
homsym (b,c))), (f
. (
homsym (a,b)))*> by
FINSEQ_2: 125
.=
<*(
homsym ((F
. b),(F
. c))), (f
. (
homsym (a,b)))*> by
Th21
.=
<*(
homsym ((F
. b),(F
. c))), (
homsym ((F
. a),(F
. b)))*> by
Th21
.= (
the_arity_of (
compsym ((F
. a),(F
. b),(F
. c)))) by
Def3
.= (the
Arity of S2
. (g
. o)) by
A6,
Th23;
end;
end;
begin
theorem ::
CATALG_1:25
Th25: for C be non
empty
set, A be
MSAlgebra over (
CatSign C) holds for a be
Element of C holds (
Args ((
idsym a),A))
=
{
{} }
proof
let C be non
empty
set, A be
MSAlgebra over (
CatSign C);
let a be
Element of C;
thus (
Args ((
idsym a),A))
= (
product (the
Sorts of A
* (
the_arity_of (
idsym a)))) by
PRALG_2: 3
.= (
product (the
Sorts of A
*
{} )) by
Def3
.=
{
{} } by
CARD_3: 10;
end;
Lm5: for C be
Category, A be
MSAlgebra over (
CatSign the
carrier of C) st for a,b be
Object of C holds (the
Sorts of A
. (
homsym (a,b)))
= (
Hom (a,b)) holds for a,b,c be
Object of C holds (
Args ((
compsym (a,b,c)),A))
= (
product
<*(
Hom (b,c)), (
Hom (a,b))*>) & (
Result ((
compsym (a,b,c)),A))
= (
Hom (a,c))
proof
let C be
Category, A be
MSAlgebra over (
CatSign the
carrier of C);
assume
A1: for a,b be
Object of C holds (the
Sorts of A
. (
homsym (a,b)))
= (
Hom (a,b));
let a,b,c be
Object of C;
A2: the
carrier of (
CatSign the
carrier of C)
= (
dom the
Sorts of A) by
PARTFUN1:def 2;
thus (
Args ((
compsym (a,b,c)),A))
= (
product (the
Sorts of A
* (
the_arity_of (
compsym (a,b,c))))) by
PRALG_2: 3
.= (
product (the
Sorts of A
*
<*(
homsym (b,c)), (
homsym (a,b))*>)) by
Def3
.= (
product
<*(the
Sorts of A
. (
homsym (b,c))), (the
Sorts of A
. (
homsym (a,b)))*>) by
A2,
FINSEQ_2: 125
.= (
product
<*(
Hom (b,c)), (the
Sorts of A
. (
homsym (a,b)))*>) by
A1
.= (
product
<*(
Hom (b,c)), (
Hom (a,b))*>) by
A1;
thus (
Result ((
compsym (a,b,c)),A))
= (the
Sorts of A
. (
the_result_sort_of (
compsym (a,b,c)))) by
PRALG_2: 3
.= (the
Sorts of A
. (
homsym (a,c))) by
Def3
.= (
Hom (a,c)) by
A1;
end;
scheme ::
CATALG_1:sch1
CatAlgEx { X,Y() -> non
empty
set , H(
set,
set) ->
set , R(
set,
set,
set,
object,
object) ->
set , I(
set) ->
set } :
ex A be
strict
MSAlgebra over (
CatSign X()) st (for a,b be
Element of X() holds (the
Sorts of A
. (
homsym (a,b)))
= H(a,b)) & (for a be
Element of X() holds ((
Den ((
idsym a),A))
.
{} )
= I(a)) & for a,b,c be
Element of X() holds for f,g be
Element of Y() st f
in H(a,b) & g
in H(b,c) holds ((
Den ((
compsym (a,b,c)),A))
.
<*g, f*>)
= R(a,b,c,g,f)
provided
A1: for a,b be
Element of X() holds H(a,b)
c= Y()
and
A2: for a be
Element of X() holds I(a)
in H(a,a)
and
A3: for a,b,c be
Element of X() holds for f,g be
Element of Y() st f
in H(a,b) & g
in H(b,c) holds R(a,b,c,g,f)
in H(a,c);
defpred
Z[
object,
object] means (($1
`1 )
= 1 & ex a be
Element of X() st $1
= (
idsym a) & ex F be
Function of
{
{} }, H(a,a) st F
= $2 & (F
.
{} )
= I(a)) or (($1
`1 )
= 2 & ex a,b,c be
Element of X() st $1
= (
compsym (a,b,c)) & ex F be
Function of (
product
<*H(b,c), H(a,b)*>), H(a,c) st F
= $2 & for f,g be
set st f
in H(a,b) & g
in H(b,c) holds (F
.
<*g, f*>)
= R(a,b,c,g,f));
set CS = (
CatSign X());
A4: for o be
object st o
in the
carrier' of CS holds ex u be
object st
Z[o, u]
proof
let o be
object;
assume
A5: o
in the
carrier' of CS;
A6:
now
assume (o
`1 )
= 1;
then
consider a be
Element of X() such that
A7: o
= (
idsym a) by
A5,
Th17;
set F = (
{}
:-> I(a));
reconsider u = F as
set;
take u, a;
thus o
= (
idsym a) by
A7;
I(a)
in H(a,a) by
A2;
then
{I(a)}
c= H(a,a) by
ZFMISC_1: 31;
then (
dom F)
=
{
{} } & (
rng F)
c= H(a,a);
then
reconsider F as
Function of
{
{} }, H(a,a) by
FUNCT_2: 2;
take F;
{}
in
{
{} } by
TARSKI:def 1;
hence F
= u & (F
.
{} )
= I(a) by
FUNCOP_1: 7;
end;
A8:
now
assume (o
`1 )
= 2;
then
consider a,b,c be
Element of X() such that
A9: o
= (
compsym (a,b,c)) by
A5,
Th18;
defpred
P[
object,
object] means ex f,g be
set st f
in H(a,b) & g
in H(b,c) & $1
=
<*g, f*> & $2
= R(a,b,c,g,f);
A10:
now
let x be
object;
assume x
in (
product
<*H(b,c), H(a,b)*>);
then
consider g,f be
object such that
A11: g
in H(b,c) & f
in H(a,b) and
A12: x
=
<*g, f*> by
FINSEQ_3: 124;
reconsider u = R(a,b,c,g,f) as
object;
take u;
H(a,b)
c= Y() & H(b,c)
c= Y() by
A1;
hence u
in H(a,c) by
A3,
A11;
thus
P[x, u] by
A11,
A12;
end;
consider F be
Function such that
A13: (
dom F)
= (
product
<*H(b,c), H(a,b)*>) & (
rng F)
c= H(a,c) and
A14: for x be
object st x
in (
product
<*H(b,c), H(a,b)*>) holds
P[x, (F
. x)] from
FUNCT_1:sch 6(
A10);
reconsider u = F as
set;
take u, a, b, c;
thus o
= (
compsym (a,b,c)) by
A9;
reconsider F as
Function of (
product
<*H(b,c), H(a,b)*>), H(a,c) by
A13,
FUNCT_2: 2;
take F;
thus F
= u;
let f,g be
set;
assume f
in H(a,b) & g
in H(b,c);
then
<*g, f*>
in (
product
<*H(b,c), H(a,b)*>) by
FINSEQ_3: 124;
then
consider f9,g9 be
set such that f9
in H(a,b) and g9
in H(b,c) and
A15:
<*g, f*>
=
<*g9, f9*> and
A16: (F
.
<*g, f*>)
= R(a,b,c,g9,f9) by
A14;
A17: (
<*g, f*>
. 1)
= g & (
<*g, f*>
. 2)
= f by
FINSEQ_1: 44;
(
<*g, f*>
. 1)
= g9 by
A15,
FINSEQ_1: 44;
hence (F
.
<*g, f*>)
= R(a,b,c,g,f) by
A15,
A16,
A17,
FINSEQ_1: 44;
end;
(o
`1 )
= 1 or (o
`1 )
= 2 by
A5,
Th16;
hence thesis by
A6,
A8;
end;
consider O be
Function such that
A18: (
dom O)
= the
carrier' of CS and
A19: for o be
object st o
in the
carrier' of CS holds
Z[o, (O
. o)] from
CLASSES1:sch 1(
A4);
reconsider O as
ManySortedSet of the
carrier' of CS by
A18,
PARTFUN1:def 2,
RELAT_1:def 18;
defpred
P[
object,
object] means ex a,b be
Element of X() st $1
= (
homsym (a,b)) & $2
= H(a,b);
A20:
now
let s be
object;
assume s
in the
carrier of CS;
then
consider a,b be
Element of X() such that
A21: s
= (
homsym (a,b)) by
Th15;
reconsider u = H(a,b) as
object;
take u;
thus
P[s, u] by
A21;
end;
consider S be
Function such that
A22: (
dom S)
= the
carrier of CS and
A23: for s be
object st s
in the
carrier of CS holds
P[s, (S
. s)] from
CLASSES1:sch 1(
A20);
reconsider S as
ManySortedSet of the
carrier of CS by
A22,
PARTFUN1:def 2,
RELAT_1:def 18;
O is
ManySortedFunction of ((S
# )
* the
Arity of CS), (S
* the
ResultSort of CS)
proof
let o be
object;
assume o
in the
carrier' of CS;
then
reconsider o as
OperSymbol of CS;
A24: (((S
# )
* the
Arity of CS)
. o)
= ((S
# )
. (
the_arity_of o)) by
FUNCT_2: 15
.= (
product (S
* (
the_arity_of o))) by
FINSEQ_2:def 5;
A25: ((S
* the
ResultSort of CS)
. o)
= (S
. (
the_result_sort_of o)) by
FUNCT_2: 15;
per cases by
Th16;
suppose (o
`1 )
= 1 & 1
<> 2;
then
consider a be
Element of X() such that
A26: o
= (
idsym a) & ex F be
Function of
{
{} }, H(a,a) st F
= (O
. o) & (F
.
{} )
= I(a) by
A19;
A27: (
the_arity_of (
idsym a))
=
{} &
{}
= (S
*
{} ) by
Def3;
A28: (
the_result_sort_of (
idsym a))
= (
homsym (a,a)) by
Def3;
consider c,b be
Element of X() such that
A29: (
homsym (a,a))
= (
homsym (c,b)) and
A30: (S
. (
homsym (a,a)))
= H(c,b) by
A23;
a
= b & a
= c by
A29,
Th13;
hence thesis by
A24,
A25,
A26,
A30,
A27,
A28,
CARD_3: 10;
end;
suppose (o
`1 )
= 2 & 1
<> 2;
then
consider a,b,c be
Element of X() such that
A31: o
= (
compsym (a,b,c)) and
A32: ex F be
Function of (
product
<*H(b,c), H(a,b)*>), H(a,c) st F
= (O
. o) & for f,g be
set st f
in H(a,b) & g
in H(b,c) holds (F
.
<*g, f*>)
= R(a,b,c,g,f) by
A19;
A33: (
the_result_sort_of (
compsym (a,b,c)))
= (
homsym (a,c)) by
Def3;
consider ax,cx be
Element of X() such that
A34: (
homsym (a,c))
= (
homsym (ax,cx)) and
A35: (S
. (
homsym (a,c)))
= H(ax,cx) by
A23;
ax
= a & cx
= c by
A34,
Th13;
then
A36: ((S
* the
ResultSort of CS)
. o)
= H(a,c) by
A31,
A35,
A33,
FUNCT_2: 15;
A37: (
the_arity_of (
compsym (a,b,c)))
=
<*(
homsym (b,c)), (
homsym (a,b))*> by
Def3;
consider a9,b9 be
Element of X() such that
A38: (
homsym (a,b))
= (
homsym (a9,b9)) and
A39: (S
. (
homsym (a,b)))
= H(a9,b9) by
A23;
consider b99,c9 be
Element of X() such that
A40: (
homsym (b,c))
= (
homsym (b99,c9)) and
A41: (S
. (
homsym (b,c)))
= H(b99,c9) by
A23;
A42: b99
= b & c9
= c by
A40,
Th13;
a9
= a & b9
= b by
A38,
Th13;
then (((S
# )
* the
Arity of CS)
. o)
= (
product
<*H(b,c), H(a,b)*>) by
A22,
A24,
A31,
A39,
A41,
A42,
A37,
FINSEQ_2: 125;
hence thesis by
A32,
A36;
end;
end;
then
reconsider O as
ManySortedFunction of ((S
# )
* the
Arity of CS), (S
* the
ResultSort of CS);
take A =
MSAlgebra (# S, O #);
hereby
let a,b be
Element of X();
consider a9,b9 be
Element of X() such that
A43: (
homsym (a,b))
= (
homsym (a9,b9)) and
A44: (S
. (
homsym (a,b)))
= H(a9,b9) by
A23;
a
= a9 by
A43,
Th13;
hence (the
Sorts of A
. (
homsym (a,b)))
= H(a,b) by
A43,
A44,
Th13;
end;
hereby
let a be
Element of X();
((
idsym a)
`1 )
= 1;
then ex b be
Element of X() st (
idsym a)
= (
idsym b) & ex F be
Function of
{
{} }, H(b,b) st F
= (O
. (
idsym a)) & (F
.
{} )
= I(b) by
A19;
hence ((
Den ((
idsym a),A))
.
{} )
= I(a) by
Th12;
end;
let a,b,c be
Element of X();
set o = (
compsym (a,b,c));
(o
`1 )
= 2;
then
consider a9,b9,c9 be
Element of X() such that
A45: o
= (
compsym (a9,b9,c9)) and
A46: ex F be
Function of (
product
<*H(b9,c9), H(a9,b9)*>), H(a9,c9) st F
= (O
. o) & for f,g be
set st f
in H(a9,b9) & g
in H(b9,c9) holds (F
.
<*g, f*>)
= R(a9,b9,c9,g,f) by
A19;
A47: c
= c9 by
A45,
Th14;
let f,g be
Element of Y();
assume
A48: f
in H(a,b) & g
in H(b,c);
a
= a9 & b
= b9 by
A45,
Th14;
hence thesis by
A46,
A47,
A48;
end;
definition
let C be
Category;
::
CATALG_1:def13
func
MSAlg C ->
strict
MSAlgebra over (
CatSign the
carrier of C) means
:
Def13: (for a,b be
Object of C holds (the
Sorts of it
. (
homsym (a,b)))
= (
Hom (a,b))) & (for a be
Object of C holds ((
Den ((
idsym a),it ))
.
{} )
= (
id a)) & for a,b,c be
Object of C holds for f,g be
Morphism of C st (
dom f)
= a & (
cod f)
= b & (
dom g)
= b & (
cod g)
= c holds ((
Den ((
compsym (a,b,c)),it ))
.
<*g, f*>)
= (g
(*) f);
uniqueness
proof
let A1,A2 be
strict
MSAlgebra over (
CatSign the
carrier of C) such that
A1: for a,b be
Object of C holds (the
Sorts of A1
. (
homsym (a,b)))
= (
Hom (a,b)) and
A2: for a be
Object of C holds ((
Den ((
idsym a),A1))
.
{} )
= (
id a) and
A3: for a,b,c be
Object of C holds for f,g be
Morphism of C st (
dom f)
= a & (
cod f)
= b & (
dom g)
= b & (
cod g)
= c holds ((
Den ((
compsym (a,b,c)),A1))
.
<*g, f*>)
= (g
(*) f) and
A4: for a,b be
Object of C holds (the
Sorts of A2
. (
homsym (a,b)))
= (
Hom (a,b)) and
A5: for a be
Object of C holds ((
Den ((
idsym a),A2))
.
{} )
= (
id a) and
A6: for a,b,c be
Object of C holds for f,g be
Morphism of C st (
dom f)
= a & (
cod f)
= b & (
dom g)
= b & (
cod g)
= c holds ((
Den ((
compsym (a,b,c)),A2))
.
<*g, f*>)
= (g
(*) f);
A7:
now
let i be
object;
assume i
in the
carrier' of (
CatSign the
carrier of C);
then
reconsider o = i as
OperSymbol of (
CatSign the
carrier of C);
per cases by
Th16;
suppose (o
`1 )
= 1;
then
consider a be
Object of C such that
A8: o
= (
idsym a) by
Th17;
A9: (
id a)
in (
Hom (a,a)) by
CAT_1: 27;
A10: (
the_result_sort_of (
idsym a))
= (
homsym (a,a)) by
Def3;
(the
Sorts of A1
. (
homsym (a,a)))
= (
Hom (a,a)) by
A1;
then (
Result ((
idsym a),A1))
= (
Hom (a,a)) by
A10,
PRALG_2: 3;
then
A11: (
dom (
Den ((
idsym a),A1)))
= (
Args ((
idsym a),A1)) by
A9,
FUNCT_2:def 1;
A12:
now
let x be
object;
assume x
in
{
{} };
then
A13: x
=
{} by
TARSKI:def 1;
then ((
Den ((
idsym a),A1))
. x)
= (
id a) by
A2;
hence ((
Den ((
idsym a),A1))
. x)
= ((
Den ((
idsym a),A2))
. x) by
A5,
A13;
end;
(the
Sorts of A2
. (
homsym (a,a)))
= (
Hom (a,a)) by
A4;
then (
Result ((
idsym a),A2))
= (
Hom (a,a)) by
A10,
PRALG_2: 3;
then
A14: (
dom (
Den ((
idsym a),A2)))
= (
Args ((
idsym a),A2)) by
A9,
FUNCT_2:def 1;
(
Args ((
idsym a),A1))
=
{
{} } & (
Args ((
idsym a),A2))
=
{
{} } by
Th25;
hence (the
Charact of A1
. i)
= (the
Charact of A2
. i) by
A8,
A11,
A14,
A12,
FUNCT_1: 2;
end;
suppose (o
`1 )
= 2;
then
consider a,b,c be
Object of C such that
A15: o
= (
compsym (a,b,c)) by
Th18;
A16:
now
assume (
product
<*(
Hom (b,c)), (
Hom (a,b))*>)
<>
{} ;
then
reconsider X = (
product
<*(
Hom (b,c)), (
Hom (a,b))*>) as non
empty
set;
set x = the
Element of X;
consider g,f be
object such that
A17: g
in (
Hom (b,c)) and
A18: f
in (
Hom (a,b)) and x
=
<*g, f*> by
FINSEQ_3: 124;
reconsider g, f as
Morphism of C by
A17,
A18;
A19: (
cod f)
= b & (
dom g)
= b by
A17,
A18,
CAT_1: 1;
(
cod g)
= c by
A17,
CAT_1: 1;
then
A20: (
cod (g
(*) f))
= c by
A19,
CAT_1: 17;
(
dom f)
= a by
A18,
CAT_1: 1;
then (
dom (g
(*) f))
= a by
A19,
CAT_1: 17;
hence (
Hom (a,c))
<>
{} by
A20,
CAT_1: 1;
end;
A21:
now
let x be
object;
assume x
in (
product
<*(
Hom (b,c)), (
Hom (a,b))*>);
then
consider g,f be
object such that
A22: g
in (
Hom (b,c)) and
A23: f
in (
Hom (a,b)) and
A24: x
=
<*g, f*> by
FINSEQ_3: 124;
reconsider g, f as
Morphism of C by
A22,
A23;
A25: (
dom g)
= b & (
cod g)
= c by
A22,
CAT_1: 1;
A26: (
dom f)
= a & (
cod f)
= b by
A23,
CAT_1: 1;
then ((
Den ((
compsym (a,b,c)),A1))
. x)
= (g
(*) f) by
A3,
A24,
A25;
hence ((
Den ((
compsym (a,b,c)),A1))
. x)
= ((
Den ((
compsym (a,b,c)),A2))
. x) by
A6,
A24,
A26,
A25;
end;
A27: (
Args ((
compsym (a,b,c)),A1))
= (
product
<*(
Hom (b,c)), (
Hom (a,b))*>) by
A1,
Lm5;
A28: (
Args ((
compsym (a,b,c)),A2))
= (
product
<*(
Hom (b,c)), (
Hom (a,b))*>) by
A4,
Lm5;
(
Result ((
compsym (a,b,c)),A2))
= (
Hom (a,c)) by
A4,
Lm5;
then
A29: (
dom (
Den ((
compsym (a,b,c)),A2)))
= (
Args ((
compsym (a,b,c)),A2)) by
A28,
A16,
FUNCT_2:def 1;
(
Result ((
compsym (a,b,c)),A1))
= (
Hom (a,c)) by
A1,
Lm5;
then (
dom (
Den ((
compsym (a,b,c)),A1)))
= (
Args ((
compsym (a,b,c)),A1)) by
A27,
A16,
FUNCT_2:def 1;
hence (the
Charact of A1
. i)
= (the
Charact of A2
. i) by
A15,
A27,
A28,
A29,
A21,
FUNCT_1: 2;
end;
end;
now
let i be
object;
assume i
in the
carrier of (
CatSign the
carrier of C);
then
consider a,b be
Object of C such that
A30: i
= (
homsym (a,b)) by
Th15;
thus (the
Sorts of A1
. i)
= (
Hom (a,b)) by
A1,
A30
.= (the
Sorts of A2
. i) by
A4,
A30;
end;
then the
Sorts of A1
= the
Sorts of A2;
hence thesis by
A7,
PBOOLE: 3;
end;
correctness
proof
deffunc
I(
Object of C) = (
id $1);
deffunc
R(
Object of C,
Object of C,
Object of C,
Morphism of C,
Morphism of C) = ($4
(*) $5);
deffunc
H(
Object of C,
Object of C) = (
Hom ($1,$2));
A31: for a be
Object of C holds
I(a)
in
H(a,a) by
CAT_1: 27;
A32:
now
let a,b,c be
Object of C, f,g be
Morphism of C;
assume that
A33: f
in
H(a,b) and
A34: g
in
H(b,c);
A35: (
cod f)
= b & (
dom g)
= b by
A33,
A34,
CAT_1: 1;
(
cod g)
= c by
A34,
CAT_1: 1;
then
A36: (
cod (g
(*) f))
= c by
A35,
CAT_1: 17;
(
dom f)
= a by
A33,
CAT_1: 1;
then (
dom (g
(*) f))
= a by
A35,
CAT_1: 17;
hence
R(a,b,c,g,f)
in
H(a,c) by
A36;
end;
A37: for a,b be
Object of C holds
H(a,b)
c= the
carrier' of C;
consider A be
strict
MSAlgebra over (
CatSign the
carrier of C) such that
A38: (for a,b be
Element of C holds (the
Sorts of A
. (
homsym (a,b)))
=
H(a,b)) & for a be
Element of C holds ((
Den ((
idsym a),A))
.
{} )
=
I(a) and
A39: for a,b,c be
Element of C holds for f,g be
Element of the
carrier' of C st f
in
H(a,b) & g
in
H(b,c) holds ((
Den ((
compsym (a,b,c)),A))
.
<*g, f*>)
=
R(a,b,c,g,f) from
CatAlgEx(
A37,
A31,
A32);
take A;
now
let a,b,c be
Object of C, f,g be
Morphism of C;
assume (
dom f)
= a & (
cod f)
= b & (
dom g)
= b & (
cod g)
= c;
then f
in (
Hom (a,b)) & g
in (
Hom (b,c));
hence ((
Den ((
compsym (a,b,c)),A))
.
<*g, f*>)
= (g
(*) f) by
A39;
end;
hence thesis by
A38;
end;
end
theorem ::
CATALG_1:26
Th26: for A be
Category, a be
Object of A holds (
Result ((
idsym a),(
MSAlg A)))
= (
Hom (a,a))
proof
let A be
Category, a be
Object of A;
thus (
Result ((
idsym a),(
MSAlg A)))
= (the
Sorts of (
MSAlg A)
. (
the_result_sort_of (
idsym a))) by
PRALG_2: 3
.= (the
Sorts of (
MSAlg A)
. (
homsym (a,a))) by
Def3
.= (
Hom (a,a)) by
Def13;
end;
theorem ::
CATALG_1:27
Th27: for A be
Category, a,b,c be
Object of A holds (
Args ((
compsym (a,b,c)),(
MSAlg A)))
= (
product
<*(
Hom (b,c)), (
Hom (a,b))*>) & (
Result ((
compsym (a,b,c)),(
MSAlg A)))
= (
Hom (a,c))
proof
let A be
Category, a,b,c be
Object of A;
for a,b be
Object of A holds (the
Sorts of (
MSAlg A)
. (
homsym (a,b)))
= (
Hom (a,b)) by
Def13;
hence thesis by
Lm5;
end;
registration
let C be
Category;
cluster (
MSAlg C) ->
disjoint_valued
feasible;
coherence
proof
hereby
let x,y be
object;
assume that
A1: x
<> y and
A2: (the
Sorts of (
MSAlg C)
. x)
meets (the
Sorts of (
MSAlg C)
. y);
consider z be
object such that
A3: z
in (the
Sorts of (
MSAlg C)
. x) and
A4: z
in (the
Sorts of (
MSAlg C)
. y) by
A2,
XBOOLE_0: 3;
(
dom the
Sorts of (
MSAlg C))
= the
carrier of (
CatSign the
carrier of C) by
PARTFUN1:def 2;
then
reconsider x, y as
SortSymbol of (
CatSign the
carrier of C) by
A3,
A4,
FUNCT_1:def 2;
consider a,b be
Object of C such that
A5: x
= (
homsym (a,b)) by
Th15;
A6: z
in (
Hom (a,b)) by
A3,
A5,
Def13;
consider c,d be
Object of C such that
A7: y
= (
homsym (c,d)) by
Th15;
A8: z
in (
Hom (c,d)) by
A4,
A7,
Def13;
reconsider z as
Morphism of C by
A6;
A9: (
dom z)
= a & (
cod z)
= b by
A6,
CAT_1: 1;
(
dom z)
= c by
A8,
CAT_1: 1;
hence contradiction by
A1,
A5,
A7,
A8,
A9,
CAT_1: 1;
end;
let o be
OperSymbol of (
CatSign the
carrier of C);
per cases by
Th16;
suppose (o
`1 )
= 1;
then
consider a be
Object of C such that
A10: o
= (
idsym a) by
Th17;
(
Result (o,(
MSAlg C)))
= (
Hom (a,a)) by
A10,
Th26;
hence thesis by
CAT_1: 27;
end;
suppose (o
`1 )
= 2;
then
consider a,b,c be
Object of C such that
A11: o
= (
compsym (a,b,c)) by
Th18;
set A = the
Element of (
Args (o,(
MSAlg C)));
assume
A12: (
Args (o,(
MSAlg C)))
<>
{} ;
(
Args (o,(
MSAlg C)))
= (
product
<*(
Hom (b,c)), (
Hom (a,b))*>) by
A11,
Th27;
then
A13: ex g,f be
object st g
in (
Hom (b,c)) & f
in (
Hom (a,b)) & A
=
<*g, f*> by
A12,
FINSEQ_3: 124;
(
Result (o,(
MSAlg C)))
= (
Hom (a,c)) by
A11,
Th27;
hence thesis by
A13,
CAT_1: 24;
end;
end;
end
theorem ::
CATALG_1:28
Th28: for C1,C2 be
Category, F be
Functor of C1, C2 holds (F
-MSF (the
carrier of (
CatSign the
carrier of C1),the
Sorts of (
MSAlg C1))) is
ManySortedFunction of (
MSAlg C1), ((
MSAlg C2)
| ((
CatSign the
carrier of C1),(
Upsilon F),(
Psi F)))
proof
let C1,C2 be
Category, F be
Functor of C1, C2;
set S1 = (
CatSign the
carrier of C1), S2 = (
CatSign the
carrier of C2);
set A1 = (
MSAlg C1), A2 = (
MSAlg C2);
set f = (
Upsilon F), g = (
Psi F), B1 = (A2
| (S1,f,g));
set H = (F
-MSF (the
carrier of S1,the
Sorts of A1));
let i be
object;
assume i
in the
carrier of S1;
then
reconsider s = i as
SortSymbol of S1;
consider a,b be
Object of C1 such that
A1: s
= (
homsym (a,b)) by
Th15;
(f,g)
form_morphism_between (S1,S2) by
Th24;
then the
Sorts of B1
= (the
Sorts of A2
* f) by
INSTALG1:def 3;
then
A2: (the
Sorts of A2
. (f
. s))
= (the
Sorts of B1
. s) by
FUNCT_2: 15;
(f
. s)
= (
homsym ((F
. a),(F
. b))) by
A1,
Th21;
then
A3: (the
Sorts of A2
. (f
. s))
= (
Hom ((F
. a),(F
. b))) by
Def13;
A4: (the
Sorts of A1
. s)
= (
Hom (a,b)) by
A1,
Def13;
(H
. s)
= (F
| (the
Sorts of A1
. s)) by
Def1;
then (H
. s)
= (
hom (F,a,b)) by
A4;
hence thesis by
A2,
A4,
A3;
end;
theorem ::
CATALG_1:29
Th29: for C be
Category, a,b,c be
Object of C holds for x be
set holds x
in (
Args ((
compsym (a,b,c)),(
MSAlg C))) iff ex g,f be
Morphism of C st x
=
<*g, f*> & (
dom f)
= a & (
cod f)
= b & (
dom g)
= b & (
cod g)
= c
proof
let C be
Category, a,b,c be
Object of C, x be
set;
set A = (
MSAlg C);
for a,b be
Object of C holds (the
Sorts of A
. (
homsym (a,b)))
= (
Hom (a,b)) by
Def13;
then
A1: (
Args ((
compsym (a,b,c)),A))
= (
product
<*(
Hom (b,c)), (
Hom (a,b))*>) by
Lm5;
hereby
assume x
in (
Args ((
compsym (a,b,c)),A));
then
consider g,f be
object such that
A2: g
in (
Hom (b,c)) & f
in (
Hom (a,b)) and
A3: x
=
<*g, f*> by
A1,
FINSEQ_3: 124;
reconsider g, f as
Morphism of C by
A2;
take g, f;
thus x
=
<*g, f*> by
A3;
thus (
dom f)
= a & (
cod f)
= b & (
dom g)
= b & (
cod g)
= c by
A2,
CAT_1: 1;
end;
given g,f be
Morphism of C such that
A4: x
=
<*g, f*> and
A5: (
dom f)
= a & (
cod f)
= b & (
dom g)
= b & (
cod g)
= c;
f
in (
Hom (a,b)) & g
in (
Hom (b,c)) by
A5;
hence thesis by
A1,
A4,
FINSEQ_3: 124;
end;
theorem ::
CATALG_1:30
Th30: for C1,C2 be
Category, F be
Functor of C1, C2 holds for a,b,c be
Object of C1 holds for f,g be
Morphism of C1 st f
in (
Hom (a,b)) & g
in (
Hom (b,c)) holds for x be
Element of (
Args ((
compsym (a,b,c)),(
MSAlg C1))) st x
=
<*g, f*> holds for H be
ManySortedFunction of (
MSAlg C1), ((
MSAlg C2)
| ((
CatSign the
carrier of C1),(
Upsilon F),(
Psi F))) st H
= (F
-MSF (the
carrier of (
CatSign the
carrier of C1),the
Sorts of (
MSAlg C1))) holds (H
# x)
=
<*(F
. g), (F
. f)*>
proof
let C1,C2 be
Category, F be
Functor of C1, C2;
set CS1 = (
CatSign the
carrier of C1), CS2 = (
CatSign the
carrier of C2);
set A1 = (
MSAlg C1), A2 = (
MSAlg C2);
set u = (
Upsilon F), p = (
Psi F);
set B = (A2
| (CS1,u,p));
let a,b,c be
Object of C1;
set o = (
compsym (a,b,c));
let f,g be
Morphism of C1 such that
A1: f
in (
Hom (a,b)) and
A2: g
in (
Hom (b,c));
let x be
Element of (
Args (o,A1)) such that
A3: x
=
<*g, f*>;
(F
. g)
in (
Hom ((F
. b),(F
. c))) by
A2,
CAT_1: 81;
then
A4: (
dom (F
. g))
= (F
. b) & (
cod (F
. g))
= (F
. c) by
CAT_1: 1;
(F
. f)
in (
Hom ((F
. a),(F
. b))) by
A1,
CAT_1: 81;
then (
dom (F
. f))
= (F
. a) & (
cod (F
. f))
= (F
. b) by
CAT_1: 1;
then
A5:
<*(F
. g), (F
. f)*>
in (
Args ((
compsym ((F
. a),(F
. b),(F
. c))),A2)) by
A4,
Th29;
A6: (
dom g)
= b & (
cod g)
= c by
A2,
CAT_1: 1;
(
dom f)
= a & (
cod f)
= b by
A1,
CAT_1: 1;
then
A7: x
in (
Args (o,A1)) by
A3,
A6,
Th29;
let H be
ManySortedFunction of A1, B such that
A8: H
= (F
-MSF (the
carrier of CS1,the
Sorts of A1));
(the
Sorts of A1
. (
homsym (b,c)))
= (
Hom (b,c)) by
Def13;
then (H
. (
homsym (b,c)))
= (F
| (
Hom (b,c))) by
A8,
Def1;
then
A9: ((H
. (
homsym (b,c)))
. g)
= (F
. g) by
A2,
FUNCT_1: 49;
A10: (
dom
<*g, f*>)
= (
Seg 2) by
FINSEQ_1: 89;
then
A11: 1
in (
dom
<*g, f*>) by
FINSEQ_1: 2,
TARSKI:def 2;
(the
Sorts of A1
. (
homsym (a,b)))
= (
Hom (a,b)) by
Def13;
then (H
. (
homsym (a,b)))
= (F
| (
Hom (a,b))) by
A8,
Def1;
then
A12: ((H
. (
homsym (a,b)))
. f)
= (F
. f) by
A1,
FUNCT_1: 49;
A13: 2
in (
dom
<*g, f*>) by
A10,
FINSEQ_1: 2,
TARSKI:def 2;
(u,p)
form_morphism_between (CS1,CS2) by
Th24;
then
A14: (
Args (o,B))
= (
Args ((p
. o),A2)) by
INSTALG1: 24
.= (
Args ((
compsym ((F
. a),(F
. b),(F
. c))),A2)) by
Th23;
then
consider g9,f9 be
Morphism of C2 such that
A15: (H
# x)
=
<*g9, f9*> and (
dom f9)
= (F
. a) and (
cod f9)
= (F
. b) and (
dom g9)
= (F
. b) and (
cod g9)
= (F
. c) by
A5,
Th29;
A16: (
<*g9, f9*>
. 1)
= g9 by
FINSEQ_1: 44;
A17: (
the_arity_of o)
=
<*(
homsym (b,c)), (
homsym (a,b))*> by
Def3;
then (
<*g, f*>
. 1)
= g & ((
the_arity_of o)
/. 1)
= (
homsym (b,c)) by
FINSEQ_1: 44,
FINSEQ_4: 17;
then
A18: (
<*g9, f9*>
. 1)
= (F
. g) by
A3,
A7,
A5,
A14,
A15,
A9,
A11,
MSUALG_3: 24;
(
<*g, f*>
. 2)
= f & ((
the_arity_of o)
/. 2)
= (
homsym (a,b)) by
A17,
FINSEQ_1: 44,
FINSEQ_4: 17;
then (
<*g9, f9*>
. 2)
= (F
. f) by
A3,
A7,
A5,
A14,
A15,
A12,
A13,
MSUALG_3: 24;
hence thesis by
A15,
A18,
A16,
FINSEQ_1: 44;
end;
theorem ::
CATALG_1:31
Th31: for C be
Category, a,b,c be
Object of C, f,g be
Morphism of C st f
in (
Hom (a,b)) & g
in (
Hom (b,c)) holds ((
Den ((
compsym (a,b,c)),(
MSAlg C)))
.
<*g, f*>)
= (g
(*) f)
proof
let C be
Category, a,b,c be
Object of C, f,g be
Morphism of C;
assume that
A1: f
in (
Hom (a,b)) and
A2: g
in (
Hom (b,c));
A3: (
dom g)
= b & (
cod g)
= c by
A2,
CAT_1: 1;
(
dom f)
= a & (
cod f)
= b by
A1,
CAT_1: 1;
hence thesis by
A3,
Def13;
end;
theorem ::
CATALG_1:32
for C be
Category, a,b,c,d be
Object of C, f,g,h be
Morphism of C st f
in (
Hom (a,b)) & g
in (
Hom (b,c)) & h
in (
Hom (c,d)) holds ((
Den ((
compsym (a,c,d)),(
MSAlg C)))
.
<*h, ((
Den ((
compsym (a,b,c)),(
MSAlg C)))
.
<*g, f*>)*>)
= ((
Den ((
compsym (a,b,d)),(
MSAlg C)))
.
<*((
Den ((
compsym (b,c,d)),(
MSAlg C)))
.
<*h, g*>), f*>)
proof
let C be
Category, a,b,c,d be
Object of C, f,g,h be
Morphism of C;
assume that
A1: f
in (
Hom (a,b)) and
A2: g
in (
Hom (b,c)) and
A3: h
in (
Hom (c,d));
A4: (
cod g)
= c by
A2,
CAT_1: 1;
A5: ((
Den ((
compsym (b,c,d)),(
MSAlg C)))
.
<*h, g*>)
= (h
(*) g) by
A2,
A3,
Th31;
A6: (
cod f)
= b by
A1,
CAT_1: 1;
A7: (
dom h)
= c by
A3,
CAT_1: 1;
(
cod h)
= d by
A3,
CAT_1: 1;
then
A8: (
cod (h
(*) g))
= d by
A4,
A7,
CAT_1: 17;
A9: (
dom g)
= b by
A2,
CAT_1: 1;
then (
dom (h
(*) g))
= b by
A4,
A7,
CAT_1: 17;
then
A10: (h
(*) g)
in (
Hom (b,d)) by
A8;
(
dom f)
= a by
A1,
CAT_1: 1;
then
A11: (
dom (g
(*) f))
= a by
A6,
A9,
CAT_1: 17;
(
cod (g
(*) f))
= c by
A6,
A9,
A4,
CAT_1: 17;
then
A12: (g
(*) f)
in (
Hom (a,c)) by
A11;
((
Den ((
compsym (a,b,c)),(
MSAlg C)))
.
<*g, f*>)
= (g
(*) f) by
A1,
A2,
Th31;
hence ((
Den ((
compsym (a,c,d)),(
MSAlg C)))
.
<*h, ((
Den ((
compsym (a,b,c)),(
MSAlg C)))
.
<*g, f*>)*>)
= (h
(*) (g
(*) f)) by
A3,
A12,
Th31
.= ((h
(*) g)
(*) f) by
A6,
A9,
A4,
A7,
CAT_1: 18
.= ((
Den ((
compsym (a,b,d)),(
MSAlg C)))
.
<*((
Den ((
compsym (b,c,d)),(
MSAlg C)))
.
<*h, g*>), f*>) by
A1,
A5,
A10,
Th31;
end;
theorem ::
CATALG_1:33
for C be
Category, a,b be
Object of C, f be
Morphism of C st f
in (
Hom (a,b)) holds ((
Den ((
compsym (a,b,b)),(
MSAlg C)))
.
<*(
id b), f*>)
= f & ((
Den ((
compsym (a,a,b)),(
MSAlg C)))
.
<*f, (
id a)*>)
= f
proof
let C be
Category, a,b be
Object of C, f be
Morphism of C;
assume
A1: f
in (
Hom (a,b));
then (
dom f)
= a by
CAT_1: 1;
then
A2: (f
(*) (
id a))
= f by
CAT_1: 22;
(
cod f)
= b by
A1,
CAT_1: 1;
then
A3: ((
id b)
(*) f)
= f by
CAT_1: 21;
(
id b)
in (
Hom (b,b)) & (
id a)
in (
Hom (a,a)) by
CAT_1: 27;
hence thesis by
A1,
A3,
A2,
Th31;
end;
theorem ::
CATALG_1:34
for C1,C2 be
Category, F be
Functor of C1, C2 holds ex H be
ManySortedFunction of (
MSAlg C1), ((
MSAlg C2)
| ((
CatSign the
carrier of C1),(
Upsilon F),(
Psi F))) st H
= (F
-MSF (the
carrier of (
CatSign the
carrier of C1),the
Sorts of (
MSAlg C1))) & H
is_homomorphism ((
MSAlg C1),((
MSAlg C2)
| ((
CatSign the
carrier of C1),(
Upsilon F),(
Psi F))))
proof
let C1,C2 be
Category, F be
Functor of C1, C2;
set S1 = (
CatSign the
carrier of C1), S2 = (
CatSign the
carrier of C2);
set A1 = (
MSAlg C1), A2 = (
MSAlg C2);
set f = (
Upsilon F), G = (
Psi F);
set B1 = (A2
| (S1,f,G));
A1: (f,G)
form_morphism_between (S1,S2) by
Th24;
reconsider H = (F
-MSF (the
carrier of S1,the
Sorts of A1)) as
ManySortedFunction of A1, B1 by
Th28;
take H;
thus H
= (F
-MSF (the
carrier of S1,the
Sorts of A1));
let o be
OperSymbol of S1;
assume
A2: (
Args (o,A1))
<>
{} ;
per cases by
Th16;
suppose (o
`1 )
= 1;
then
consider a be
Object of C1 such that
A3: o
= (
idsym a) by
Th17;
let x be
Element of (
Args (o,A1));
A4: (
Args ((G
. o),A2))
= (
Args (o,B1)) by
A1,
INSTALG1: 24;
A5: (G
. o)
= (
idsym (F
. a)) by
A3,
Th22;
then (
Args ((G
. o),A2))
=
{
{} } by
Th25;
then
A6: (H
# x)
=
{} by
A4,
TARSKI:def 1;
reconsider h = (
id a) as
Morphism of a, a;
(
dom (
id a))
= a & (
cod (
id a))
= a by
CAT_1: 58;
then
A7: (
id a)
in (
Hom (a,a));
(
Args (o,A1))
=
{
{} } by
A3,
Th25;
then x
=
{} by
TARSKI:def 1;
hence ((H
. (
the_result_sort_of o))
. ((
Den (o,A1))
. x))
= ((H
. (
the_result_sort_of o))
. h) by
A3,
Def13
.= ((H
. (
homsym (a,a)))
. h) by
A3,
Def3
.= ((F
| (the
Sorts of A1
. (
homsym (a,a))))
. h) by
Def1
.= ((F
| (
Hom (a,a)))
. h) by
Def13
.= ((
hom (F,a,a))
. h)
.= (F
. h) by
A7,
CAT_1: 88
.= (
id (F
. a)) by
CAT_1: 71
.= ((
Den ((G
. o),A2))
. (H
# x)) by
A5,
A6,
Def13
.= ((
Den (o,B1))
. (H
# x)) by
Th24,
INSTALG1: 23;
end;
suppose
A8: (o
`1 )
= 2;
let x be
Element of (
Args (o,A1));
consider a,b,c be
Object of C1 such that
A9: o
= (
compsym (a,b,c)) by
A8,
Th18;
A10: (G
. o)
= (
compsym ((F
. a),(F
. b),(F
. c))) by
A9,
Th23;
consider g,h be
Morphism of C1 such that
A11: x
=
<*g, h*> and
A12: (
dom h)
= a and
A13: (
cod h)
= b and
A14: (
dom g)
= b and
A15: (
cod g)
= c by
A2,
A9,
Th29;
A16: g
in (
Hom (b,c)) & h
in (
Hom (a,b)) by
A12,
A13,
A14,
A15;
(
dom (g
(*) h))
= a & (
cod (g
(*) h))
= c by
A12,
A13,
A14,
A15,
CAT_1: 17;
then
A17: (g
(*) h)
in (
Hom (a,c));
then
reconsider gh = (g
(*) h) as
Morphism of a, c by
CAT_1:def 5;
A18: (
dom (F
. h))
= (F
. a) & (
cod (F
. h))
= (F
. b) by
A12,
A13,
CAT_1: 72;
A19: (
dom (F
. g))
= (F
. b) & (
cod (F
. g))
= (F
. c) by
A14,
A15,
CAT_1: 72;
thus ((H
. (
the_result_sort_of o))
. ((
Den (o,A1))
. x))
= ((H
. (
the_result_sort_of o))
. gh) by
A9,
A11,
A12,
A13,
A14,
A15,
Def13
.= ((H
. (
homsym (a,c)))
. gh) by
A9,
Def3
.= ((F
| (the
Sorts of A1
. (
homsym (a,c))))
. gh) by
Def1
.= ((F
| (
Hom (a,c)))
. gh) by
Def13
.= ((
hom (F,a,c))
. gh)
.= (F
. gh) by
A17,
CAT_1: 88
.= ((F
. g)
(*) (F
. h)) by
A13,
A14,
CAT_1: 64
.= ((
Den ((G
. o),A2))
.
<*(F
. g), (F
. h)*>) by
A10,
A18,
A19,
Def13
.= ((
Den ((G
. o),A2))
. (H
# x)) by
A9,
A11,
A16,
Th30
.= ((
Den (o,B1))
. (H
# x)) by
Th24,
INSTALG1: 23;
end;
end;