:: CATALG_1 semantic presentation

definition

let c₁ be set ;
let c₂, c₃ be Function;
func c₃ -MSF c₁,c₂ -> ManySortedFunction of a₁ means :Def1: :: CATALG_1:def 1
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = a₃ | (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th1: :: CATALG_1:1

for b₁ being set
for b₂ being ManySortedSet of b₁ holds (id (Union b₂)) -MSF b₁,b₂ = id b₂

proof end;

theorem Th2: :: CATALG_1:2

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄, b₅ being Function st rngs (b₄ -MSF b₁,b₂) c= b₃ holds
(b₅ * b₄) -MSF b₁,b₂ = (b₅ -MSF b₁,b₃) ** (b₄ -MSF b₁,b₂)

proof end;

theorem Th3: :: CATALG_1:3

for b₁ being Function
for b₂ being set
for b₃, b₄ being ManySortedSet of b₂ st ( for b₅ being set st b₅ in b₂ holds
( b₃ . b₅ c= dom b₁ & b₁ .: (b₃ . b₅) c= b₄ . b₅ ) ) holds
b₁ -MSF b₂,b₃ is ManySortedFunction of b₃,b₄

proof end;

theorem Th4: :: CATALG_1:4

for b₁ being set
for b₂ being Nat
for b₃ being FinSequence holds
( b₃ in b₂ -tuples_on b₁ iff ( len b₃ = b₂ & rng b₃ c= b₁ ) )

proof end;

theorem Th5: :: CATALG_1:5

for b₁ being set
for b₂ being Nat
for b₃ being FinSequence of b₁ holds
( b₃ in b₂ -tuples_on b₁ iff len b₃ = b₂ )

proof end;

theorem Th6: :: CATALG_1:6

for b₁ being set
for b₂ being Nat holds b₂ -tuples_on b₁ c= b₁ *

proof end;

E4: now

let c₁, c₂ be set ;
assume <*c₁*> = <*c₂*> ;
then <*c₁*> . 1 = c₂ by FINSEQ_1:57;
hence c₁ = c₂ by FINSEQ_1:57;

end;

theorem Th7: :: CATALG_1:7

for b₁ being set
for b₂ being Nat holds
( ( b₂ <> 0 & b₁ = {} ) iff b₂ -tuples_on b₁ = {} )

proof end;

theorem Th8: :: CATALG_1:8

for b₁, b₂ being set holds
( b₂ in 1 -tuples_on b₁ iff ex b₃ being set st
( b₃ in b₁ & b₂ = <*b₃*> ) )

proof end;

theorem Th9: :: CATALG_1:9

for b₁, b₂ being set st <*b₂*> in 1 -tuples_on b₁ holds
b₂ in b₁

proof end;

theorem Th10: :: CATALG_1:10

for b₁, b₂ being set holds
( b₂ in 2 -tuples_on b₁ iff ex b₃, b₄ being set st
( b₃ in b₁ & b₄ in b₁ & b₂ = <*b₃,b₄*> ) )

proof end;

theorem Th11: :: CATALG_1:11

for b₁, b₂, b₃ being set st <*b₂,b₃*> in 2 -tuples_on b₁ holds
( b₂ in b₁ & b₃ in b₁ )

proof end;

theorem Th12: :: CATALG_1:12

for b₁, b₂ being set holds
( b₂ in 3 -tuples_on b₁ iff ex b₃, b₄, b₅ being set st
( b₃ in b₁ & b₄ in b₁ & b₅ in b₁ & b₂ = <*b₃,b₄,b₅*> ) )

proof end;

theorem Th13: :: CATALG_1:13

for b₁, b₂, b₃, b₄ being set st <*b₂,b₃,b₄*> in 3 -tuples_on b₁ holds
( b₂ in b₁ & b₃ in b₁ & b₄ in b₁ )

proof end;

definition

let c₁ be non empty ManySortedSign ;
let c₂ be MSAlgebra of c₁;
canceled;
attr a₂ is empty means :Def3: :: CATALG_1:def 3
the Sorts of a₂ is empty-yielding;

end;

:: deftheorem Def2 CATALG_1:def 2 :

:: deftheorem Def3 defines empty CATALG_1:def 3 :

registration

let c₁ be non empty ManySortedSign ;
cluster non-empty -> non empty MSAlgebra of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
cluster FreeMSA a₂ -> disjoint_valued non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
cluster strict non-empty disjoint_valued non empty MSAlgebra of a₁;
existence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non empty MSAlgebra of c₁;
cluster the Sorts of a₂ -> V3 ;
coherence by Def3;

end;

registration

cluster non empty-yielding set ;
existence

proof end;

end;

definition

let c₁ be set ;
canceled;
func CatSign c₁ -> strict ManySortedSign means :Def5: :: CATALG_1:def 5
( the carrier of a₂ = [:{0},(2 -tuples_on a₁):] & the OperSymbols of a₂ = [:{1},(1 -tuples_on a₁):] \/ [:{2},(3 -tuples_on a₁):] & ( for b₁ being set st b₁ in a₁ holds
( the Arity of a₂ . [1,<*b₁*>] = {} & the ResultSort of a₂ . [1,<*b₁*>] = [0,<*b₁,b₁*>] ) ) & ( for b₁, b₂, b₃ being set st b₁ in a₁ & b₂ in a₁ & b₃ in a₁ holds
( the Arity of a₂ . [2,<*b₁,b₂,b₃*>] = <*[0,<*b₂,b₃*>],[0,<*b₁,b₂*>]*> & the ResultSort of a₂ . [2,<*b₁,b₂,b₃*>] = [0,<*b₁,b₃*>] ) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def4 CATALG_1:def 4 :

:: deftheorem Def5 defines CatSign CATALG_1:def 5 :

registration

let c₁ be set ;
cluster CatSign a₁ -> strict feasible ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster CatSign a₁ -> non empty strict non void feasible ;
coherence

proof end;

end;

definition

mode Signature is feasible ManySortedSign ;

end;

definition

let c₁ be Signature;
attr a₁ is Categorial means :Def6: :: CATALG_1:def 6
ex b₁ being set st
( CatSign b₁ is Subsignature of a₁ & the carrier of a₁ = [:{0},(2 -tuples_on b₁):] );

end;

:: deftheorem Def6 defines Categorial CATALG_1:def 6 :

registration

cluster non empty Categorial -> non empty non void ManySortedSign ;
coherence

proof end;

end;

registration

cluster non empty strict non void Categorial ManySortedSign ;
existence

proof end;

end;

definition

mode CatSignature is Categorial Signature;

end;

definition

let c₁ be set ;
mode CatSignature of c₁ -> Signature means :Def7: :: CATALG_1:def 7
( CatSign a₁ is Subsignature of a₂ & the carrier of a₂ = [:{0},(2 -tuples_on a₁):] );
existence

proof end;

end;

:: deftheorem Def7 defines CatSignature CATALG_1:def 7 :

theorem Th14: :: CATALG_1:14

for b₁, b₂ being set
for b₃ being CatSignature of b₁ st b₃ is CatSignature of b₂ holds
b₁ = b₂

proof end;

registration

let c₁ be set ;
cluster -> Categorial CatSignature of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster -> non empty non void Categorial CatSignature of a₁;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster strict Categorial CatSignature of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
redefine func CatSign as CatSign c₁ -> strict CatSignature of a₁;
coherence

proof end;

end;

definition

let c₁ be ManySortedSign ;
func underlay c₁ -> set means :Def8: :: CATALG_1:def 8
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being set ex b₃ being Function st
( [b₂,b₃] in the carrier of a₁ \/ the OperSymbols of a₁ & b₁ in rng b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines underlay CATALG_1:def 8 :

theorem Th15: :: CATALG_1:15

for b₁ being set holds underlay (CatSign b₁) = b₁

proof end;

definition

let c₁ be ManySortedSign ;
attr a₁ is delta-concrete means :Def9: :: CATALG_1:def 9
ex b₁ being Function of NAT , NAT st
( ( for b₂ being set st b₂ in the carrier of a₁ holds
ex b₃ being Natex b₄ being FinSequence st
( b₂ = [b₃,b₄] & len b₄ = b₁ . b₃ & [:{b₃},((b₁ . b₃) -tuples_on (underlay a₁)):] c= the carrier of a₁ ) ) & ( for b₂ being set st b₂ in the OperSymbols of a₁ holds
ex b₃ being Natex b₄ being FinSequence st
( b₂ = [b₃,b₄] & len b₄ = b₁ . b₃ & [:{b₃},((b₁ . b₃) -tuples_on (underlay a₁)):] c= the OperSymbols of a₁ ) ) );

end;

:: deftheorem Def9 defines delta-concrete CATALG_1:def 9 :

registration

let c₁ be set ;
cluster CatSign a₁ -> strict feasible delta-concrete ;
coherence

proof end;

end;

registration

cluster non empty strict non void delta-concrete ManySortedSign ;
existence

proof end;

let c₁ be set ;
cluster strict Categorial delta-concrete CatSignature of a₁;
existence

proof end;

end;

theorem Th16: :: CATALG_1:16

for b₁ being delta-concrete ManySortedSign
for b₂ being set st ( b₂ in the carrier of b₁ or b₂ in the OperSymbols of b₁ ) holds
ex b₃ being Natex b₄ being FinSequence st
( b₂ = [b₃,b₄] & rng b₄ c= underlay b₁ )

proof end;

theorem Th17: :: CATALG_1:17

for b₁ being delta-concrete ManySortedSign
for b₂ being set
for b₃, b₄ being FinSequence st ( ( [b₂,b₃] in the carrier of b₁ & [b₂,b₄] in the carrier of b₁ ) or ( [b₂,b₃] in the OperSymbols of b₁ & [b₂,b₄] in the OperSymbols of b₁ ) ) holds
len b₃ = len b₄

proof end;

theorem Th18: :: CATALG_1:18

for b₁ being delta-concrete ManySortedSign
for b₂ being set
for b₃, b₄ being FinSequence st len b₄ = len b₃ & rng b₄ c= underlay b₁ holds
( ( [b₂,b₃] in the carrier of b₁ implies [b₂,b₄] in the carrier of b₁ ) & ( [b₂,b₃] in the OperSymbols of b₁ implies [b₂,b₄] in the OperSymbols of b₁ ) )

proof end;

theorem Th19: :: CATALG_1:19

for b₁ being non empty Categorial delta-concrete Signature holds b₁ is CatSignature of underlay b₁

proof end;

registration

let c₁ be non empty CatSignature;
let c₂ be SortSymbol of c₁;
cluster a₂ `2 -> Relation-like Function-like ;
coherence

proof end;

end;

registration

let c₁ be non empty delta-concrete ManySortedSign ;
let c₂ be SortSymbol of c₁;
cluster a₂ `2 -> Relation-like Function-like ;
coherence

proof end;

end;

registration

let c₁ be non void delta-concrete ManySortedSign ;
let c₂ be Element of the OperSymbols of c₁;
cluster a₂ `2 -> Relation-like Function-like ;
coherence

proof end;

end;

registration

let c₁ be non empty CatSignature;
let c₂ be SortSymbol of c₁;
cluster a₂ `2 -> Relation-like Function-like FinSequence-like ;
coherence

proof end;

end;

registration

let c₁ be non empty delta-concrete ManySortedSign ;
let c₂ be SortSymbol of c₁;
cluster a₂ `2 -> Relation-like Function-like FinSequence-like ;
coherence

proof end;

end;

registration

let c₁ be non void delta-concrete ManySortedSign ;
let c₂ be Element of the OperSymbols of c₁;
cluster a₂ `2 -> Relation-like Function-like FinSequence-like ;
coherence

proof end;

end;

definition

let c₁ be set ;
func idsym c₁ -> set equals :: CATALG_1:def 10
[1,<*a₁*>];
correctness ;
let c₂ be set ;
func homsym c₁,c₂ -> set equals :: CATALG_1:def 11
[0,<*a₁,a₂*>];
correctness ;
let c₃ be set ;
func compsym c₁,c₂,c₃ -> set equals :: CATALG_1:def 12
[2,<*a₁,a₂,a₃*>];
correctness ;

end;

:: deftheorem Def10 defines idsym CATALG_1:def 10 :

:: deftheorem Def11 defines homsym CATALG_1:def 11 :

:: deftheorem Def12 defines compsym CATALG_1:def 12 :

theorem Th20: :: CATALG_1:20

for b₁ being non empty set
for b₂ being CatSignature of b₁
for b₃ being Element of b₁ holds
( idsym b₃ in the OperSymbols of b₂ & ( for b₄ being Element of b₁ holds
( homsym b₃,b₄ in the carrier of b₂ & ( for b₅ being Element of b₁ holds compsym b₃,b₄,b₅ in the OperSymbols of b₂ ) ) ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func idsym as idsym c₂ -> OperSymbol of (CatSign a₁);
correctness by Th20;
let c₃ be Element of c₁;
redefine func homsym as homsym c₂,c₃ -> SortSymbol of (CatSign a₁);
correctness by Th20;
let c₄ be Element of c₁;
redefine func compsym as compsym c₂,c₃,c₄ -> OperSymbol of (CatSign a₁);
correctness by Th20;

end;

theorem Th21: :: CATALG_1:21

for b₁, b₂ being set st idsym b₁ = idsym b₂ holds
b₁ = b₂

proof end;

theorem Th22: :: CATALG_1:22

for b₁, b₂, b₃, b₄ being set st homsym b₁,b₃ = homsym b₂,b₄ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

theorem Th23: :: CATALG_1:23

for b₁, b₂, b₃, b₄, b₅, b₆ being set st compsym b₁,b₃,b₅ = compsym b₂,b₄,b₆ holds
( b₁ = b₂ & b₃ = b₄ & b₅ = b₆ )

proof end;

theorem Th24: :: CATALG_1:24

for b₁ being non empty set
for b₂ being CatSignature of b₁
for b₃ being SortSymbol of b₂ ex b₄, b₅ being Element of b₁ st b₃ = homsym b₄,b₅

proof end;

theorem Th25: :: CATALG_1:25

for b₁ being non empty set
for b₂ being OperSymbol of (CatSign b₁) holds
( ( b₂ `1 = 1 & len (b₂ `2 ) = 1 ) or ( b₂ `1 = 2 & len (b₂ `2 ) = 3 ) )

proof end;

theorem Th26: :: CATALG_1:26

for b₁ being non empty set
for b₂ being OperSymbol of (CatSign b₁) st ( b₂ `1 = 1 or len (b₂ `2 ) = 1 ) holds
ex b₃ being Element of b₁ st b₂ = idsym b₃

proof end;

theorem Th27: :: CATALG_1:27

for b₁ being non empty set
for b₂ being OperSymbol of (CatSign b₁) st ( b₂ `1 = 2 or len (b₂ `2 ) = 3 ) holds
ex b₃, b₄, b₅ being Element of b₁ st b₂ = compsym b₃,b₄,b₅

proof end;

theorem Th28: :: CATALG_1:28

for b₁ being non empty set
for b₂ being Element of b₁ holds
( the_arity_of (idsym b₂) = {} & the_result_sort_of (idsym b₂) = homsym b₂,b₂ ) by Def5;

theorem Th29: :: CATALG_1:29

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ holds
( the_arity_of (compsym b₂,b₃,b₄) = <*(homsym b₃,b₄),(homsym b₂,b₃)*> & the_result_sort_of (compsym b₂,b₃,b₄) = homsym b₂,b₄ ) by Def5;

definition

let c₁, c₂ be Category;
let c₃ be Functor of c₁,c₂;
func Upsilon c₃ -> Function of the carrier of (CatSign the Objects of a₁),the carrier of (CatSign the Objects of a₂) means :Def13: :: CATALG_1:def 13
for b₁ being SortSymbol of (CatSign the Objects of a₁) holds a₄ . b₁ = [0,((Obj a₃) * (b₁ `2 ))];
uniqueness

proof end;

existence

proof end;

func Psi c₃ -> Function of the OperSymbols of (CatSign the Objects of a₁),the OperSymbols of (CatSign the Objects of a₂) means :Def14: :: CATALG_1:def 14
for b₁ being OperSymbol of (CatSign the Objects of a₁) holds a₄ . b₁ = [(b₁ `1 ),((Obj a₃) * (b₁ `2 ))];
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def13 defines Upsilon CATALG_1:def 13 :

:: deftheorem Def14 defines Psi CATALG_1:def 14 :

E30: now

let c₁ be set ;
let c₂ be Function;
assume c₁ in dom c₂ ;
then ( rng <*c₁*> = {c₁} & {c₁} c= dom c₂ ) by FINSEQ_1:56, ZFMISC_1:37;
then E31: dom (c₂ * <*c₁*>) = dom <*c₁*> by RELAT_1:46
.= Seg 1 by FINSEQ_1:55 ;
then reconsider c₃ = c₂ * <*c₁*> as FinSequence by FINSEQ_1:def 2;
( 1 in {1} & <*c₁*> . 1 = c₁ ) by FINSEQ_1:57, TARSKI:def 1;
then ( len c₃ = 1 & c₃ . 1 = c₂ . c₁ ) by E31, FINSEQ_1:4, FINSEQ_1:def 3, FUNCT_1:22;
hence c₂ * <*c₁*> = <*(c₂ . c₁)*> by FINSEQ_1:57;

end;

theorem Th30: :: CATALG_1:30

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄, b₅ being Object of b₁ holds (Upsilon b₃) . (homsym b₄,b₅) = homsym (b₃ . b₄),(b₃ . b₅)

proof end;

theorem Th31: :: CATALG_1:31

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Object of b₁ holds (Psi b₃) . (idsym b₄) = idsym (b₃ . b₄)

proof end;

theorem Th32: :: CATALG_1:32

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄, b₅, b₆ being Object of b₁ holds (Psi b₃) . (compsym b₄,b₅,b₆) = compsym (b₃ . b₄),(b₃ . b₅),(b₃ . b₆)

proof end;

theorem Th33: :: CATALG_1:33

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ holds Upsilon b₃, Psi b₃ form_morphism_between CatSign the Objects of b₁, CatSign the Objects of b₂

proof end;

theorem Th34: :: CATALG_1:34

for b₁ being non empty set
for b₂ being MSAlgebra of CatSign b₁
for b₃ being Element of b₁ holds Args (idsym b₃),b₂ = {{} }

proof end;

Lemma36: for b₁ being Category
for b₂ being MSAlgebra of CatSign the Objects of b₁ st ( for b₃, b₄ being Object of b₁ holds the Sorts of b₂ . (homsym b₃,b₄) = Hom b₃,b₄ ) holds
for b₃, b₄, b₅ being Object of b₁ holds
( Args (compsym b₃,b₄,b₅),b₂ = product <*(Hom b₄,b₅),(Hom b₃,b₄)*> & Result (compsym b₃,b₄,b₅),b₂ = Hom b₃,b₅ )

proof end;

scheme :: CATALG_1:sch 1
s1{ F₁() -> non empty set , F₂() -> non empty set , F₃( set , set ) -> set , F₄( set , set , set , set , set ) -> set , F₅( set ) -> set } :

ex b₁ being strict MSAlgebra of CatSign F₁() st
( ( for b₂, b₃ being Element of F₁() holds the Sorts of b₁ . (homsym b₂,b₃) = F₃(b₂,b₃) ) & ( for b₂ being Element of F₁() holds (Den (idsym b₂),b₁) . {} = F₅(b₂) ) & ( for b₂, b₃, b₄ being Element of F₁()
for b₅, b₆ being Element of F₂() st b₅ in F₃(b₂,b₃) & b₆ in F₃(b₃,b₄) holds
(Den (compsym b₂,b₃,b₄),b₁) . <*b₆,b₅*> = F₄(b₂,b₃,b₄,b₆,b₅) ) )

provided

E37: for b₁, b₂ being Element of F₁() holds F₃(b₁,b₂) c= F₂() and
E38: for b₁ being Element of F₁() holds F₅(b₁) in F₃(b₁,b₁) and
E39: for b₁, b₂, b₃ being Element of F₁()
for b₄, b₅ being Element of F₂() st b₄ in F₃(b₁,b₂) & b₅ in F₃(b₂,b₃) holds
F₄(b₁,b₂,b₃,b₅,b₄) in F₃(b₁,b₃)

proof end;

definition

let c₁ be Category;
func MSAlg c₁ -> strict MSAlgebra of CatSign the Objects of a₁ means :Def15: :: CATALG_1:def 15
( ( for b₁, b₂ being Object of a₁ holds the Sorts of a₂ . (homsym b₁,b₂) = Hom b₁,b₂ ) & ( for b₁ being Object of a₁ holds (Den (idsym b₁),a₂) . {} = id b₁ ) & ( for b₁, b₂, b₃ being Object of a₁
for b₄, b₅ being Morphism of a₁ st dom b₄ = b₁ & cod b₄ = b₂ & dom b₅ = b₂ & cod b₅ = b₃ holds
(Den (compsym b₁,b₂,b₃),a₂) . <*b₅,b₄*> = b₅ * b₄ ) );
uniqueness

proof end;

correctness

proof end;

end;

:: deftheorem Def15 defines MSAlg CATALG_1:def 15 :

theorem Th35: :: CATALG_1:35

canceled;

theorem Th36: :: CATALG_1:36

for b₁ being Category
for b₂ being Object of b₁ holds Result (idsym b₂),(MSAlg b₁) = Hom b₂,b₂

proof end;

theorem Th37: :: CATALG_1:37

for b₁ being Category
for b₂, b₃, b₄ being Object of b₁ holds
( Args (compsym b₂,b₃,b₄),(MSAlg b₁) = product <*(Hom b₃,b₄),(Hom b₂,b₃)*> & Result (compsym b₂,b₃,b₄),(MSAlg b₁) = Hom b₂,b₄ )

proof end;

registration

let c₁ be Category;
cluster MSAlg a₁ -> strict feasible disjoint_valued ;
coherence

proof end;

end;

theorem Th38: :: CATALG_1:38

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ holds b₃ -MSF the carrier of (CatSign the Objects of b₁),the Sorts of (MSAlg b₁) is ManySortedFunction of (MSAlg b₁),((MSAlg b₂) | (CatSign the Objects of b₁),(Upsilon b₃),(Psi b₃))

proof end;

theorem Th39: :: CATALG_1:39

for b₁ being Category
for b₂, b₃, b₄ being Object of b₁
for b₅ being set holds
( b₅ in Args (compsym b₂,b₃,b₄),(MSAlg b₁) iff ex b₆, b₇ being Morphism of b₁ st
( b₅ = <*b₆,b₇*> & dom b₇ = b₂ & cod b₇ = b₃ & dom b₆ = b₃ & cod b₆ = b₄ ) )

proof end;

theorem Th40: :: CATALG_1:40

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄, b₅, b₆ being Object of b₁
for b₇, b₈ being Morphism of b₁ st b₇ in Hom b₄,b₅ & b₈ in Hom b₅,b₆ holds
for b₉ being Element of Args (compsym b₄,b₅,b₆),(MSAlg b₁) st b₉ = <*b₈,b₇*> holds
for b₁₀ being ManySortedFunction of (MSAlg b₁),((MSAlg b₂) | (CatSign the Objects of b₁),(Upsilon b₃),(Psi b₃)) st b₁₀ = b₃ -MSF the carrier of (CatSign the Objects of b₁),the Sorts of (MSAlg b₁) holds
b₁₀ # b₉ = <*(b₃ . b₈),(b₃ . b₇)*>

proof end;

theorem Th41: :: CATALG_1:41

canceled;

theorem Th42: :: CATALG_1:42

for b₁ being Category
for b₂, b₃, b₄ being Object of b₁
for b₅, b₆ being Morphism of b₁ st b₅ in Hom b₂,b₃ & b₆ in Hom b₃,b₄ holds
(Den (compsym b₂,b₃,b₄),(MSAlg b₁)) . <*b₆,b₅*> = b₆ * b₅

proof end;

theorem Th43: :: CATALG_1:43

for b₁ being Category
for b₂, b₃, b₄, b₅ being Object of b₁
for b₆, b₇, b₈ being Morphism of b₁ st b₆ in Hom b₂,b₃ & b₇ in Hom b₃,b₄ & b₈ in Hom b₄,b₅ holds
(Den (compsym b₂,b₄,b₅),(MSAlg b₁)) . <*b₈,((Den (compsym b₂,b₃,b₄),(MSAlg b₁)) . <*b₇,b₆*>)*> = (Den (compsym b₂,b₃,b₅),(MSAlg b₁)) . <*((Den (compsym b₃,b₄,b₅),(MSAlg b₁)) . <*b₈,b₇*>),b₆*>

proof end;

theorem Th44: :: CATALG_1:44

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄ being Morphism of b₁ st b₄ in Hom b₂,b₃ holds
( (Den (compsym b₂,b₃,b₃),(MSAlg b₁)) . <*(id b₃),b₄*> = b₄ & (Den (compsym b₂,b₂,b₃),(MSAlg b₁)) . <*b₄,(id b₂)*> = b₄ )

proof end;

theorem Th45: :: CATALG_1:45

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ ex b₄ being ManySortedFunction of (MSAlg b₁),((MSAlg b₂) | (CatSign the Objects of b₁),(Upsilon b₃),(Psi b₃)) st
( b₄ = b₃ -MSF the carrier of (CatSign the Objects of b₁),the Sorts of (MSAlg b₁) & b₄ is_homomorphism MSAlg b₁,(MSAlg b₂) | (CatSign the Objects of b₁),(Upsilon b₃),(Psi b₃) )

proof end;