:: by Grzegorz Bancerek

::

:: Received January 28, 1997

:: Copyright (c) 1997-2016 Association of Mizar Users

definition

let I be set ;

let A, f be Function;

ex b_{1} being ManySortedFunction of I st

for i being object st i in I holds

b_{1} . i = f | (A . i)

for b_{1}, b_{2} being ManySortedFunction of I st ( for i being object st i in I holds

b_{1} . i = f | (A . i) ) & ( for i being object st i in I holds

b_{2} . i = f | (A . i) ) holds

b_{1} = b_{2}

end;
let A, f be Function;

func f -MSF (I,A) -> ManySortedFunction of I means :Def1: :: CATALG_1:def 1

for i being object st i in I holds

it . i = f | (A . i);

existence for i being object st i in I holds

it . i = f | (A . i);

ex b

for i being object st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines -MSF CATALG_1:def 1 :

for I being set

for A, f being Function

for b_{4} being ManySortedFunction of I holds

( b_{4} = f -MSF (I,A) iff for i being object st i in I holds

b_{4} . i = f | (A . i) );

for I being set

for A, f being Function

for b

( b

b

theorem :: CATALG_1:2

for I being set

for A, B being ManySortedSet of I

for f, g being Function st rngs (f -MSF (I,A)) c= B holds

(g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A))

for A, B being ManySortedSet of I

for f, g being Function st rngs (f -MSF (I,A)) c= B holds

(g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A))

proof end;

theorem :: CATALG_1:3

for f being Function

for I being set

for A, B being ManySortedSet of I st ( for i being 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

for I being set

for A, B being ManySortedSet of I st ( for i being 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 end;

Lm1: now :: thesis: for x, y being set st <*x*> = <*y*> holds

x = y

x = y

let x, y be set ; :: thesis: ( <*x*> = <*y*> implies x = y )

assume <*x*> = <*y*> ; :: thesis: x = y

then <*x*> . 1 = y by FINSEQ_1:40;

hence x = y by FINSEQ_1:40; :: thesis: verum

end;
assume <*x*> = <*y*> ; :: thesis: x = y

then <*x*> . 1 = y by FINSEQ_1:40;

hence x = y by FINSEQ_1:40; :: thesis: verum

:: deftheorem Def2 defines empty CATALG_1:def 2 :

for S being non empty ManySortedSign

for A being MSAlgebra over S holds

( A is empty iff the Sorts of A is V3() );

for S being non empty ManySortedSign

for A being MSAlgebra over S holds

( A is empty iff the Sorts of A is V3() );

registration

let S be non empty ManySortedSign ;

coherence

for b_{1} being MSAlgebra over S st b_{1} is non-empty holds

not b_{1} is empty
;

end;
coherence

for b

not b

registration

let S be non empty non void ManySortedSign ;

existence

ex b_{1} being MSAlgebra over S st

( b_{1} is strict & b_{1} is non-empty & b_{1} is disjoint_valued )

end;
existence

ex b

( b

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non empty MSAlgebra over S;

coherence

not the Sorts of A is empty-yielding by Def2;

end;
let A be non empty MSAlgebra over S;

coherence

not the Sorts of A is empty-yielding by Def2;

definition

let A be set ;

ex b_{1} being strict ManySortedSign st

( the carrier of b_{1} = [:{0},(2 -tuples_on A):] & the carrier' of b_{1} = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds

( the Arity of b_{1} . [1,<*a*>] = {} & the ResultSort of b_{1} . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds

( the Arity of b_{1} . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b_{1} . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) )

uniqueness

for b_{1}, b_{2} being strict ManySortedSign st the carrier of b_{1} = [:{0},(2 -tuples_on A):] & the carrier' of b_{1} = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds

( the Arity of b_{1} . [1,<*a*>] = {} & the ResultSort of b_{1} . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds

( the Arity of b_{1} . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b_{1} . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) & the carrier of b_{2} = [:{0},(2 -tuples_on A):] & the carrier' of b_{2} = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds

( the Arity of b_{2} . [1,<*a*>] = {} & the ResultSort of b_{2} . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds

( the Arity of b_{2} . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b_{2} . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) holds

b_{1} = b_{2};

end;
func CatSign A -> strict ManySortedSign means :Def3: :: CATALG_1:def 3

( 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 being 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 being 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 ( 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 being 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 being 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*>] ) ) );

ex b

( the carrier of b

( the Arity of b

( the Arity of b

proof end;

correctness uniqueness

for b

( the Arity of b

( the Arity of b

( the Arity of b

( the Arity of b

b

proof end;

:: deftheorem Def3 defines CatSign CATALG_1:def 3 :

for A being set

for b_{2} being strict ManySortedSign holds

( b_{2} = CatSign A iff ( the carrier of b_{2} = [:{0},(2 -tuples_on A):] & the carrier' of b_{2} = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds

( the Arity of b_{2} . [1,<*a*>] = {} & the ResultSort of b_{2} . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds

( the Arity of b_{2} . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b_{2} . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) ) );

for A being set

for b

( b

( the Arity of b

( the Arity of b

registration
end;

registration
end;

definition

let S be Signature;

end;
attr S is Categorial means :Def4: :: CATALG_1:def 4

ex A being set st

( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] );

ex A being set st

( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] );

:: deftheorem Def4 defines Categorial CATALG_1:def 4 :

for S being Signature holds

( S is Categorial iff ex A being set st

( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ) );

for S being Signature holds

( S is Categorial iff ex A being set st

( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ) );

registration

coherence

for b_{1} being non empty Signature st b_{1} is Categorial holds

not b_{1} is void

end;
for b

not b

proof end;

registration

existence

ex b_{1} being Signature st

( b_{1} is Categorial & not b_{1} is empty & b_{1} is strict )

end;
ex b

( b

proof end;

definition

let A be set ;

ex b_{1} being Signature st

( CatSign A is Subsignature of b_{1} & the carrier of b_{1} = [:{0},(2 -tuples_on A):] )

end;
mode CatSignature of A -> Signature means :Def5: :: CATALG_1:def 5

( CatSign A is Subsignature of it & the carrier of it = [:{0},(2 -tuples_on A):] );

existence ( CatSign A is Subsignature of it & the carrier of it = [:{0},(2 -tuples_on A):] );

ex b

( CatSign A is Subsignature of b

proof end;

:: deftheorem Def5 defines CatSignature CATALG_1:def 5 :

for A being set

for b_{2} being Signature holds

( b_{2} is CatSignature of A iff ( CatSign A is Subsignature of b_{2} & the carrier of b_{2} = [:{0},(2 -tuples_on A):] ) );

for A being set

for b

( b

registration
end;

registration

let A be non empty set ;

coherence

for b_{1} being CatSignature of A holds not b_{1} is empty

end;
coherence

for b

proof end;

registration
end;

definition

let A be set ;

:: original: CatSign

redefine func CatSign A -> strict CatSignature of A;

coherence

CatSign A is strict CatSignature of A

end;
:: original: CatSign

redefine func CatSign A -> strict CatSignature of A;

coherence

CatSign A is strict CatSignature of A

proof end;

definition

let S be ManySortedSign ;

assume A1: for x being object st x in proj2 ( the carrier of S \/ the carrier' of S) holds

x is Function ;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex a being set ex f being Function st

( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex a being set ex f being Function st

( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) ) & ( for x being object holds

( x in b_{2} iff ex a being set ex f being Function st

( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) ) holds

b_{1} = b_{2}

end;
assume A1: for x being object st x in proj2 ( the carrier of S \/ the carrier' of S) holds

x is Function ;

func underlay S -> set means :Def6: :: CATALG_1:def 6

for x being object holds

( x in it iff ex a being set ex f being Function st

( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) );

existence for x being object holds

( x in it iff ex a being set ex f being Function st

( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) );

ex b

for x being object holds

( x in b

( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) )

proof end;

uniqueness for b

( x in b

( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) ) & ( for x being object holds

( x in b

( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) ) holds

b

proof end;

:: deftheorem Def6 defines underlay CATALG_1:def 6 :

for S being ManySortedSign st ( for x being object st x in proj2 ( the carrier of S \/ the carrier' of S) holds

x is Function ) holds

for b_{2} being set holds

( b_{2} = underlay S iff for x being object holds

( x in b_{2} iff ex a being set ex f being Function st

( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) );

for S being ManySortedSign st ( for x being object st x in proj2 ( the carrier of S \/ the carrier' of S) holds

x is Function ) holds

for b

( b

( x in b

( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) );

definition

let S be ManySortedSign ;

end;
attr S is delta-concrete means :Def7: :: CATALG_1:def 7

ex f being sequence of NAT st

( ( for s being object st s in the carrier of S holds

ex i being Element of NAT ex p being FinSequence st

( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) ) & ( for o being object st o in the carrier' of S holds

ex i being Element of NAT ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) ) );

ex f being sequence of NAT st

( ( for s being object st s in the carrier of S holds

ex i being Element of NAT ex p being FinSequence st

( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) ) & ( for o being object st o in the carrier' of S holds

ex i being Element of NAT ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) ) );

:: deftheorem Def7 defines delta-concrete CATALG_1:def 7 :

for S being ManySortedSign holds

( S is delta-concrete iff ex f being sequence of NAT st

( ( for s being object st s in the carrier of S holds

ex i being Element of NAT ex p being FinSequence st

( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) ) & ( for o being object st o in the carrier' of S holds

ex i being Element of NAT ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) ) ) );

for S being ManySortedSign holds

( S is delta-concrete iff ex f being sequence of NAT st

( ( for s being object st s in the carrier of S holds

ex i being Element of NAT ex p being FinSequence st

( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) ) & ( for o being object st o in the carrier' of S holds

ex i being Element of NAT ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) ) ) );

Lm2: for A being set

for x being object st x in proj2 ( the carrier of (CatSign A) \/ the carrier' of (CatSign A)) holds

x is Function

proof end;

registration

existence

ex b_{1} being CatSignature st

( b_{1} is delta-concrete & not b_{1} is empty & b_{1} is strict )

existence

ex b_{1} being CatSignature of A st

( b_{1} is delta-concrete & b_{1} is strict )

end;
ex b

( b

proof end;

let A be set ;existence

ex b

( b

proof end;

registration
end;

registration

existence

ex b_{1} being CatSignature st

( b_{1} is delta-concrete & not b_{1} is empty & b_{1} is strict )

existence

ex b_{1} being CatSignature of A st

( b_{1} is delta-concrete & b_{1} is strict )

end;
ex b

( b

proof end;

let A be set ;existence

ex b

( b

proof end;

Lm3: for S being delta-concrete ManySortedSign

for x being object st x in proj2 ( the carrier of S \/ the carrier' of S) holds

x is Function

proof end;

theorem Th7: :: CATALG_1:7

for S being delta-concrete ManySortedSign

for x being set st ( x in the carrier of S or x in the carrier' of S ) holds

ex i being Element of NAT ex p being FinSequence st

( x = [i,p] & rng p c= underlay S )

for x being set st ( x in the carrier of S or x in the carrier' of S ) holds

ex i being Element of NAT ex p being FinSequence st

( x = [i,p] & rng p c= underlay S )

proof end;

theorem :: CATALG_1:8

for S being delta-concrete ManySortedSign

for i being set

for p1, p2 being 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

for i being set

for p1, p2 being 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 end;

theorem :: CATALG_1:9

for S being delta-concrete ManySortedSign

for i being set

for p1, p2 being 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 ) )

for i being set

for p1, p2 being 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 end;

registration

let S be non empty CatSignature;

let s be SortSymbol of S;

coherence

for b_{1} being set st b_{1} = s `2 holds

( b_{1} is Relation-like & b_{1} is Function-like )

end;
let s be SortSymbol of S;

coherence

for b

( b

proof end;

registration

let S be non empty delta-concrete ManySortedSign ;

let s be SortSymbol of S;

coherence

for b_{1} being set st b_{1} = s `2 holds

( b_{1} is Relation-like & b_{1} is Function-like )

end;
let s be SortSymbol of S;

coherence

for b

( b

proof end;

registration

let S be non void delta-concrete ManySortedSign ;

let o be Element of the carrier' of S;

coherence

for b_{1} being set st b_{1} = o `2 holds

( b_{1} is Relation-like & b_{1} is Function-like )

end;
let o be Element of the carrier' of S;

coherence

for b

( b

proof end;

registration

let S be non empty CatSignature;

let s be SortSymbol of S;

coherence

for b_{1} being Function st b_{1} = s `2 holds

b_{1} is FinSequence-like

end;
let s be SortSymbol of S;

coherence

for b

b

proof end;

registration

let S be non empty delta-concrete ManySortedSign ;

let s be SortSymbol of S;

coherence

for b_{1} being Function st b_{1} = s `2 holds

b_{1} is FinSequence-like

end;
let s be SortSymbol of S;

coherence

for b

b

proof end;

registration

let S be non void delta-concrete ManySortedSign ;

let o be Element of the carrier' of S;

coherence

for b_{1} being Function st b_{1} = o `2 holds

b_{1} is FinSequence-like

end;
let o be Element of the carrier' of S;

coherence

for b

b

proof end;

definition

let a be set ;

correctness

coherence

[1,<*a*>] is set ;

;

let b be set ;

correctness

coherence

[0,<*a,b*>] is set ;

;

let c be set ;

correctness

coherence

[2,<*a,b,c*>] is set ;

;

end;
correctness

coherence

[1,<*a*>] is set ;

;

let b be set ;

correctness

coherence

[0,<*a,b*>] is set ;

;

let c be set ;

correctness

coherence

[2,<*a,b,c*>] is set ;

;

:: deftheorem defines compsym CATALG_1:def 10 :

for a, b, c being set holds compsym (a,b,c) = [2,<*a,b,c*>];

for a, b, c being set holds compsym (a,b,c) = [2,<*a,b,c*>];

theorem Th11: :: CATALG_1:11

for A being non empty set

for S being CatSignature of A

for a being Element of A holds

( idsym a in the carrier' of S & ( for b being Element of A holds

( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) ) )

for S being CatSignature of A

for a being Element of A holds

( idsym a in the carrier' of S & ( for b being Element of A holds

( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) ) )

proof 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

coherence

idsym a is OperSymbol of (CatSign A);

by Th11;

let b be Element of A;

:: original: homsym

redefine func homsym (a,b) -> SortSymbol of (CatSign A);

correctness

coherence

homsym (a,b) is SortSymbol of (CatSign A);

by Th11;

let c be Element of A;

:: original: compsym

redefine func compsym (a,b,c) -> OperSymbol of (CatSign A);

correctness

coherence

compsym (a,b,c) is OperSymbol of (CatSign A);

by Th11;

end;
let a be Element of A;

:: original: idsym

redefine func idsym a -> OperSymbol of (CatSign A);

correctness

coherence

idsym a is OperSymbol of (CatSign A);

by Th11;

let b be Element of A;

:: original: homsym

redefine func homsym (a,b) -> SortSymbol of (CatSign A);

correctness

coherence

homsym (a,b) is SortSymbol of (CatSign A);

by Th11;

let c be Element of A;

:: original: compsym

redefine func compsym (a,b,c) -> OperSymbol of (CatSign A);

correctness

coherence

compsym (a,b,c) is OperSymbol of (CatSign A);

by Th11;

theorem Th14: :: CATALG_1:14

for a1, b1, a2, b2, a3, b3 being set st compsym (a1,a2,a3) = compsym (b1,b2,b3) holds

( a1 = b1 & a2 = b2 & a3 = b3 )

( a1 = b1 & a2 = b2 & a3 = b3 )

proof end;

theorem Th15: :: CATALG_1:15

for A being non empty set

for S being CatSignature of A

for s being SortSymbol of S ex a, b being Element of A st s = homsym (a,b)

for S being CatSignature of A

for s being SortSymbol of S ex a, b being Element of A st s = homsym (a,b)

proof end;

theorem Th16: :: CATALG_1:16

for A being non empty set

for o being OperSymbol of (CatSign A) holds

( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) )

for o being OperSymbol of (CatSign A) holds

( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) )

proof end;

theorem Th17: :: CATALG_1:17

for A being non empty set

for o being OperSymbol of (CatSign A) st ( o `1 = 1 or len (o `2) = 1 ) holds

ex a being Element of A st o = idsym a

for o being OperSymbol of (CatSign A) st ( o `1 = 1 or len (o `2) = 1 ) holds

ex a being Element of A st o = idsym a

proof end;

theorem Th18: :: CATALG_1:18

for A being non empty set

for o being OperSymbol of (CatSign A) st ( o `1 = 2 or len (o `2) = 3 ) holds

ex a, b, c being Element of A st o = compsym (a,b,c)

for o being OperSymbol of (CatSign A) st ( o `1 = 2 or len (o `2) = 3 ) holds

ex a, b, c being Element of A st o = compsym (a,b,c)

proof end;

theorem :: CATALG_1:19

theorem :: CATALG_1:20

definition

let C1, C2 be Category;

let F be Functor of C1,C2;

for b_{1}, b_{2} being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) st ( for s being SortSymbol of (CatSign the carrier of C1) holds b_{1} . s = [0,((Obj F) * (s `2))] ) & ( for s being SortSymbol of (CatSign the carrier of C1) holds b_{2} . s = [0,((Obj F) * (s `2))] ) holds

b_{1} = b_{2}

ex b_{1} being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) st

for s being SortSymbol of (CatSign the carrier of C1) holds b_{1} . s = [0,((Obj F) * (s `2))]

for b_{1}, b_{2} being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) st ( for o being OperSymbol of (CatSign the carrier of C1) holds b_{1} . o = [(o `1),((Obj F) * (o `2))] ) & ( for o being OperSymbol of (CatSign the carrier of C1) holds b_{2} . o = [(o `1),((Obj F) * (o `2))] ) holds

b_{1} = b_{2}

ex b_{1} being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) st

for o being OperSymbol of (CatSign the carrier of C1) holds b_{1} . o = [(o `1),((Obj F) * (o `2))]

end;
let F be Functor of C1,C2;

func Upsilon F -> Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) means :Def11: :: CATALG_1:def 11

for s being SortSymbol of (CatSign the carrier of C1) holds it . s = [0,((Obj F) * (s `2))];

uniqueness for s being SortSymbol of (CatSign the carrier of C1) holds it . s = [0,((Obj F) * (s `2))];

for b

b

proof end;

existence ex b

for s being SortSymbol of (CatSign the carrier of C1) holds b

proof end;

func Psi F -> Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) means :Def12: :: CATALG_1:def 12

for o being OperSymbol of (CatSign the carrier of C1) holds it . o = [(o `1),((Obj F) * (o `2))];

uniqueness for o being OperSymbol of (CatSign the carrier of C1) holds it . o = [(o `1),((Obj F) * (o `2))];

for b

b

proof end;

existence ex b

for o being OperSymbol of (CatSign the carrier of C1) holds b

proof end;

:: deftheorem Def11 defines Upsilon CATALG_1:def 11 :

for C1, C2 being Category

for F being Functor of C1,C2

for b_{4} being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) holds

( b_{4} = Upsilon F iff for s being SortSymbol of (CatSign the carrier of C1) holds b_{4} . s = [0,((Obj F) * (s `2))] );

for C1, C2 being Category

for F being Functor of C1,C2

for b

( b

:: deftheorem Def12 defines Psi CATALG_1:def 12 :

for C1, C2 being Category

for F being Functor of C1,C2

for b_{4} being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) holds

( b_{4} = Psi F iff for o being OperSymbol of (CatSign the carrier of C1) holds b_{4} . o = [(o `1),((Obj F) * (o `2))] );

for C1, C2 being Category

for F being Functor of C1,C2

for b

( b

Lm4: now :: thesis: for x being set

for f being Function st x in dom f holds

f * <*x*> = <*(f . x)*>

for f being Function st x in dom f holds

f * <*x*> = <*(f . x)*>

let x be set ; :: thesis: for f being Function st x in dom f holds

f * <*x*> = <*(f . x)*>

let f be Function; :: thesis: ( x in dom f implies f * <*x*> = <*(f . x)*> )

assume x in dom f ; :: thesis: f * <*x*> = <*(f . x)*>

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; :: thesis: verum

end;
f * <*x*> = <*(f . x)*>

let f be Function; :: thesis: ( x in dom f implies f * <*x*> = <*(f . x)*> )

assume x in dom f ; :: thesis: f * <*x*> = <*(f . x)*>

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; :: thesis: verum

theorem Th21: :: CATALG_1:21

for C1, C2 being Category

for F being Functor of C1,C2

for a, b being Object of C1 holds (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b))

for F being Functor of C1,C2

for a, b being Object of C1 holds (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b))

proof end;

theorem Th22: :: CATALG_1:22

for C1, C2 being Category

for F being Functor of C1,C2

for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a)

for F being Functor of C1,C2

for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a)

proof end;

theorem Th23: :: CATALG_1:23

for C1, C2 being Category

for F being Functor of C1,C2

for a, b, c being Object of C1 holds (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c))

for F being Functor of C1,C2

for a, b, c being Object of C1 holds (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c))

proof end;

theorem Th24: :: CATALG_1:24

for C1, C2 being Category

for F being Functor of C1,C2 holds Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2

for F being Functor of C1,C2 holds Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2

proof end;

theorem Th25: :: CATALG_1:25

for C being non empty set

for A being MSAlgebra over CatSign C

for a being Element of C holds Args ((idsym a),A) = {{}}

for A being MSAlgebra over CatSign C

for a being Element of C holds Args ((idsym a),A) = {{}}

proof end;

Lm5: for C being Category

for A being MSAlgebra over CatSign the carrier of C st ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) holds

for a, b, c being 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 end;

scheme :: CATALG_1:sch 1

CatAlgEx{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( set , set ) -> set , F_{4}( set , set , set , object , object ) -> set , F_{5}( set ) -> set } :

CatAlgEx{ F

ex A being strict MSAlgebra over CatSign F_{1}() st

( ( for a, b being Element of F_{1}() holds the Sorts of A . (homsym (a,b)) = F_{3}(a,b) ) & ( for a being Element of F_{1}() holds (Den ((idsym a),A)) . {} = F_{5}(a) ) & ( for a, b, c being Element of F_{1}()

for f, g being Element of F_{2}() st f in F_{3}(a,b) & g in F_{3}(b,c) holds

(Den ((compsym (a,b,c)),A)) . <*g,f*> = F_{4}(a,b,c,g,f) ) )

provided( ( for a, b being Element of F

for f, g being Element of F

(Den ((compsym (a,b,c)),A)) . <*g,f*> = F

A1:
for a, b being Element of F_{1}() holds F_{3}(a,b) c= F_{2}()
and

A2: for a being Element of F_{1}() holds F_{5}(a) in F_{3}(a,a)
and

A3: for a, b, c being Element of F_{1}()

for f, g being Element of F_{2}() st f in F_{3}(a,b) & g in F_{3}(b,c) holds

F_{4}(a,b,c,g,f) in F_{3}(a,c)

A2: for a being Element of F

A3: for a, b, c being Element of F

for f, g being Element of F

F

proof end;

definition

let C be Category;

for b_{1}, b_{2} being strict MSAlgebra over CatSign the carrier of C st ( for a, b being Object of C holds the Sorts of b_{1} . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b_{1})) . {} = id a ) & ( for a, b, c being Object of C

for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds

(Den ((compsym (a,b,c)),b_{1})) . <*g,f*> = g (*) f ) & ( for a, b being Object of C holds the Sorts of b_{2} . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b_{2})) . {} = id a ) & ( for a, b, c being Object of C

for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds

(Den ((compsym (a,b,c)),b_{2})) . <*g,f*> = g (*) f ) holds

b_{1} = b_{2}

existence

ex b_{1} being strict MSAlgebra over CatSign the carrier of C st

( ( for a, b being Object of C holds the Sorts of b_{1} . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b_{1})) . {} = id a ) & ( for a, b, c being Object of C

for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds

(Den ((compsym (a,b,c)),b_{1})) . <*g,f*> = g (*) f ) );

end;
func MSAlg C -> strict MSAlgebra over CatSign the carrier of C means :Def13: :: CATALG_1:def 13

( ( for a, b being Object of C holds the Sorts of it . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),it)) . {} = id a ) & ( for a, b, c being Object of C

for f, g being 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 ( ( for a, b being Object of C holds the Sorts of it . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),it)) . {} = id a ) & ( for a, b, c being Object of C

for f, g being 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 ) );

for b

for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds

(Den ((compsym (a,b,c)),b

for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds

(Den ((compsym (a,b,c)),b

b

proof end;

correctness existence

ex b

( ( for a, b being Object of C holds the Sorts of b

for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds

(Den ((compsym (a,b,c)),b

proof end;

:: deftheorem Def13 defines MSAlg CATALG_1:def 13 :

for C being Category

for b_{2} being strict MSAlgebra over CatSign the carrier of C holds

( b_{2} = MSAlg C iff ( ( for a, b being Object of C holds the Sorts of b_{2} . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b_{2})) . {} = id a ) & ( for a, b, c being Object of C

for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds

(Den ((compsym (a,b,c)),b_{2})) . <*g,f*> = g (*) f ) ) );

for C being Category

for b

( b

for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds

(Den ((compsym (a,b,c)),b

theorem Th27: :: CATALG_1:27

for A being Category

for a, b, c being 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) )

for a, b, c being 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 end;

registration
end;

theorem Th28: :: CATALG_1:28

for C1, C2 being Category

for F being 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)))

for F being 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 end;

theorem Th29: :: CATALG_1:29

for C being Category

for a, b, c being Object of C

for x being set holds

( x in Args ((compsym (a,b,c)),(MSAlg C)) iff ex g, f being Morphism of C st

( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) )

for a, b, c being Object of C

for x being set holds

( x in Args ((compsym (a,b,c)),(MSAlg C)) iff ex g, f being Morphism of C st

( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) )

proof end;

theorem Th30: :: CATALG_1:30

for C1, C2 being Category

for F being Functor of C1,C2

for a, b, c being Object of C1

for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds

for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds

for H being 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)*>

for F being Functor of C1,C2

for a, b, c being Object of C1

for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds

for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds

for H being 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 end;

theorem Th31: :: CATALG_1:31

for C being Category

for a, b, c being Object of C

for f, g being 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

for a, b, c being Object of C

for f, g being 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 end;

theorem :: CATALG_1:32

for C being Category

for a, b, c, d being Object of C

for f, g, h being 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*>

for a, b, c, d being Object of C

for f, g, h being 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 end;

theorem :: CATALG_1:33

for C being Category

for a, b being Object of C

for f being 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 )

for a, b being Object of C

for f being 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 end;

theorem :: CATALG_1:34

for C1, C2 being Category

for F being Functor of C1,C2 ex H being 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)) )

for F being Functor of C1,C2 ex H being 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 end;