:: CATALG_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let I be set ;
let A, f be Function;
func f -MSF I,A -> ManySortedFunction of I means :Def1: :: CATALG_1:def 1
for i being set st i in I holds
it . i = f | (A . i);
existence
ex b1 being ManySortedFunction of I st
for i being set st i in I holds
b1 . i = f | (A . i)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of I st ( for i being set st i in I holds
b1 . i = f | (A . i) ) & ( for i being set st i in I holds
b2 . i = f | (A . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines -MSF CATALG_1:def 1 :
for I being set
for A, f being Function
for b4 being ManySortedFunction of I holds
( b4 = f -MSF I,A iff for i being set st i in I holds
b4 . i = f | (A . i) );

theorem :: CATALG_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I holds (id (Union A)) -MSF I,A = id A
proof end;

theorem :: CATALG_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: CATALG_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th4: :: CATALG_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for i being Nat
for p being FinSequence holds
( p in i -tuples_on A iff ( len p = i & rng p c= A ) )
proof end;

theorem Th5: :: CATALG_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for i being Nat
for p being FinSequence of A holds
( p in i -tuples_on A iff len p = i )
proof end;

theorem :: CATALG_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for i being Nat holds i -tuples_on A c= A *
proof end;

Lm1: now
let x, y be set ; :: thesis: ( <*x*> = <*y*> implies x = y )
assume <*x*> = <*y*> ; :: thesis: x = y
then <*x*> . 1 = y by FINSEQ_1:57;
hence x = y by FINSEQ_1:57; :: thesis: verum
end;

theorem Th7: :: CATALG_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for i being Nat holds
( ( i <> 0 & A = {} ) iff i -tuples_on A = {} )
proof end;

theorem Th8: :: CATALG_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, x being set holds
( x in 1 -tuples_on A iff ex a being set st
( a in A & x = <*a*> ) )
proof end;

theorem :: CATALG_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, a being set st <*a*> in 1 -tuples_on A holds
a in A
proof end;

theorem Th10: :: CATALG_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, x being set holds
( x in 2 -tuples_on A iff ex a, b being set st
( a in A & b in A & x = <*a,b*> ) )
proof end;

theorem Th11: :: CATALG_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, a, b being set st <*a,b*> in 2 -tuples_on A holds
( a in A & b in A )
proof end;

theorem Th12: :: CATALG_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, x being set holds
( x in 3 -tuples_on A iff ex a, b, c being set st
( a in A & b in A & c in A & x = <*a,b,c*> ) )
proof end;

theorem :: CATALG_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, a, b, c being set st <*a,b,c*> in 3 -tuples_on A holds
( a in A & b in A & c in A )
proof end;

definition
let S be non empty ManySortedSign ;
let A be MSAlgebra of S;
canceled;
attr A is empty means :Def3: :: CATALG_1:def 3
the Sorts of A is empty-yielding;
end;

:: deftheorem CATALG_1:def 2 :
canceled;

:: deftheorem Def3 defines empty CATALG_1:def 3 :
for S being non empty ManySortedSign
for A being MSAlgebra of S holds
( A is empty iff the Sorts of A is empty-yielding );

registration
let S be non empty ManySortedSign ;
cluster non-empty -> non empty MSAlgebra of S;
coherence
for b1 being MSAlgebra of S st b1 is non-empty holds
not b1 is empty
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V2 ManySortedSet of the carrier of S;
cluster FreeMSA X -> disjoint_valued non empty ;
coherence
FreeMSA X is disjoint_valued
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
cluster strict non-empty disjoint_valued non empty MSAlgebra of S;
existence
ex b1 being MSAlgebra of S st
( b1 is strict & b1 is non-empty & b1 is disjoint_valued )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non empty MSAlgebra of S;
cluster the Sorts of A -> V3 ;
coherence
not the Sorts of A is empty-yielding
by Def3;
end;

registration
cluster non empty-yielding set ;
existence
not for b1 being Function holds b1 is empty-yielding
proof end;
end;

definition
let A be set ;
canceled;
func CatSign A -> strict ManySortedSign means :Def5: :: CATALG_1:def 5
( the carrier of it = [:{0},(2 -tuples_on A):] & the OperSymbols 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
ex b1 being strict ManySortedSign st
( the carrier of b1 = [:{0},(2 -tuples_on A):] & the OperSymbols of b1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b1 . [1,<*a*>] = {} & the ResultSort of b1 . [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 b1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) )
proof end;
correctness
uniqueness
for b1, b2 being strict ManySortedSign st the carrier of b1 = [:{0},(2 -tuples_on A):] & the OperSymbols of b1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b1 . [1,<*a*>] = {} & the ResultSort of b1 . [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 b1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) & the carrier of b2 = [:{0},(2 -tuples_on A):] & the OperSymbols of b2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b2 . [1,<*a*>] = {} & the ResultSort of b2 . [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 b2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b2 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem CATALG_1:def 4 :
canceled;

:: deftheorem Def5 defines CatSign CATALG_1:def 5 :
for A being set
for b2 being strict ManySortedSign holds
( b2 = CatSign A iff ( the carrier of b2 = [:{0},(2 -tuples_on A):] & the OperSymbols of b2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b2 . [1,<*a*>] = {} & the ResultSort of b2 . [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 b2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b2 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) ) );

registration
let A be set ;
cluster CatSign A -> strict feasible ;
coherence
CatSign A is feasible
proof end;
end;

registration
let A be non empty set ;
cluster CatSign A -> non empty strict non void feasible ;
coherence
( not CatSign A is empty & not CatSign A is void )
proof end;
end;

definition
mode Signature is feasible ManySortedSign ;
end;

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

:: deftheorem Def6 defines Categorial CATALG_1:def 6 :
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
cluster non empty Categorial -> non empty non void ManySortedSign ;
coherence
for b1 being non empty Signature st b1 is Categorial holds
not b1 is void
proof end;
end;

registration
cluster non empty strict non void Categorial ManySortedSign ;
existence
ex b1 being Signature st
( b1 is Categorial & not b1 is empty & b1 is strict )
proof end;
end;

definition
mode CatSignature is Categorial Signature;
end;

definition
let A be set ;
mode CatSignature of A -> Signature means :Def7: :: CATALG_1:def 7
( CatSign A is Subsignature of it & the carrier of it = [:{0},(2 -tuples_on A):] );
existence
ex b1 being Signature st
( CatSign A is Subsignature of b1 & the carrier of b1 = [:{0},(2 -tuples_on A):] )
proof end;
end;

:: deftheorem Def7 defines CatSignature CATALG_1:def 7 :
for A being set
for b2 being Signature holds
( b2 is CatSignature of A iff ( CatSign A is Subsignature of b2 & the carrier of b2 = [:{0},(2 -tuples_on A):] ) );

theorem :: CATALG_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A1, A2 being set
for S being CatSignature of A1 st S is CatSignature of A2 holds
A1 = A2
proof end;

registration
let A be set ;
cluster -> Categorial CatSignature of A;
coherence
for b1 being CatSignature of A holds b1 is Categorial
proof end;
end;

registration
let A be non empty set ;
cluster -> non empty non void Categorial CatSignature of A;
coherence
for b1 being CatSignature of A holds not b1 is empty
proof end;
end;

registration
let A be set ;
cluster strict Categorial CatSignature of A;
existence
ex b1 being CatSignature of A st b1 is strict
proof end;
end;

definition
let A be set ;
:: original: CatSign
redefine func CatSign A -> strict CatSignature of A;
coherence
CatSign A is strict CatSignature of A
proof end;
end;

definition
let S be ManySortedSign ;
func underlay S -> set means :Def8: :: CATALG_1:def 8
for x being set holds
( x in it iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the OperSymbols of S & x in rng f ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the OperSymbols of S & x in rng f ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the OperSymbols of S & x in rng f ) ) ) & ( for x being set holds
( x in b2 iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the OperSymbols of S & x in rng f ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines underlay CATALG_1:def 8 :
for S being ManySortedSign
for b2 being set holds
( b2 = underlay S iff for x being set holds
( x in b2 iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the OperSymbols of S & x in rng f ) ) );

theorem Th15: :: CATALG_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds underlay (CatSign A) = A
proof end;

definition
let S be ManySortedSign ;
attr S is delta-concrete means :Def9: :: CATALG_1:def 9
ex f being Function of NAT , NAT st
( ( for s being set st s in the carrier of S holds
ex i being 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 set st o in the OperSymbols of S holds
ex i being Nat ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the OperSymbols of S ) ) );
end;

:: deftheorem Def9 defines delta-concrete CATALG_1:def 9 :
for S being ManySortedSign holds
( S is delta-concrete iff ex f being Function of NAT , NAT st
( ( for s being set st s in the carrier of S holds
ex i being 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 set st o in the OperSymbols of S holds
ex i being Nat ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the OperSymbols of S ) ) ) );

registration
let A be set ;
cluster CatSign A -> strict feasible delta-concrete ;
coherence
CatSign A is delta-concrete
proof end;
end;

registration
cluster non empty strict non void delta-concrete ManySortedSign ;
existence
ex b1 being CatSignature st
( b1 is delta-concrete & not b1 is empty & b1 is strict )
proof end;
let A be set ;
cluster strict Categorial delta-concrete CatSignature of A;
existence
ex b1 being CatSignature of A st
( b1 is delta-concrete & b1 is strict )
proof end;
end;

theorem Th16: :: CATALG_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being delta-concrete ManySortedSign
for x being set st ( x in the carrier of S or x in the OperSymbols of S ) holds
ex i being Nat ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )
proof end;

theorem :: CATALG_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 OperSymbols of S & [i,p2] in the OperSymbols of S ) ) holds
len p1 = len p2
proof end;

theorem :: CATALG_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 OperSymbols of S implies [i,p2] in the OperSymbols of S ) )
proof end;

theorem :: CATALG_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty Categorial delta-concrete Signature holds S is CatSignature of underlay S
proof end;

registration
let S be non empty CatSignature;
let s be SortSymbol of S;
cluster s `2 -> Relation-like Function-like ;
coherence
( s `2 is Relation-like & s `2 is Function-like )
proof 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
( s `2 is Relation-like & s `2 is Function-like )
proof end;
end;

registration
let S be non void delta-concrete ManySortedSign ;
let o be Element of the OperSymbols of S;
cluster o `2 -> Relation-like Function-like ;
coherence
( o `2 is Relation-like & o `2 is Function-like )
proof end;
end;

registration
let S be non empty CatSignature;
let s be SortSymbol of S;
cluster s `2 -> Relation-like Function-like FinSequence-like ;
coherence
s `2 is FinSequence-like
proof end;
end;

registration
let S be non empty delta-concrete ManySortedSign ;
let s be SortSymbol of S;
cluster s `2 -> Relation-like Function-like FinSequence-like ;
coherence
s `2 is FinSequence-like
proof end;
end;

registration
let S be non void delta-concrete ManySortedSign ;
let o be Element of the OperSymbols of S;
cluster o `2 -> Relation-like Function-like FinSequence-like ;
coherence
o `2 is FinSequence-like
proof end;
end;

definition
let a be set ;
func idsym a -> set equals :: CATALG_1:def 10
[1,<*a*>];
correctness
coherence
[1,<*a*>] is set
;
;
let b be set ;
func homsym a,b -> set equals :: CATALG_1:def 11
[0,<*a,b*>];
correctness
coherence
[0,<*a,b*>] is set
;
;
let c be set ;
func compsym a,b,c -> set equals :: CATALG_1:def 12
[2,<*a,b,c*>];
correctness
coherence
[2,<*a,b,c*>] is set
;
;
end;

:: deftheorem defines idsym CATALG_1:def 10 :
for a being set holds idsym a = [1,<*a*>];

:: deftheorem defines homsym CATALG_1:def 11 :
for a, b being set holds homsym a,b = [0,<*a,b*>];

:: deftheorem defines compsym CATALG_1:def 12 :
for a, b, c being set holds compsym a,b,c = [2,<*a,b,c*>];

theorem Th20: :: CATALG_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for S being CatSignature of A
for a being Element of A holds
( idsym a in the OperSymbols 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 OperSymbols 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 Th20;
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 Th20;
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 Th20;
end;

theorem Th21: :: CATALG_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set st idsym a = idsym b holds
a = b
proof end;

theorem Th22: :: CATALG_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, b1, a2, b2 being set st homsym a1,a2 = homsym b1,b2 holds
( a1 = b1 & a2 = b2 )
proof end;

theorem Th23: :: CATALG_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th24: :: CATALG_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th25: :: CATALG_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th26: :: CATALG_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th27: :: CATALG_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th28: :: CATALG_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for a being Element of A holds
( the_arity_of (idsym a) = {} & the_result_sort_of (idsym a) = homsym a,a ) by Def5;

theorem Th29: :: CATALG_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for a, b, c being 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 Def5;

definition
let C1, C2 be Category;
let F be Functor of C1,C2;
func Upsilon F -> Function of the carrier of (CatSign the Objects of C1),the carrier of (CatSign the Objects of C2) means :Def13: :: CATALG_1:def 13
for s being SortSymbol of (CatSign the Objects of C1) holds it . s = [0,((Obj F) * (s `2 ))];
uniqueness
for b1, b2 being Function of the carrier of (CatSign the Objects of C1),the carrier of (CatSign the Objects of C2) st ( for s being SortSymbol of (CatSign the Objects of C1) holds b1 . s = [0,((Obj F) * (s `2 ))] ) & ( for s being SortSymbol of (CatSign the Objects of C1) holds b2 . s = [0,((Obj F) * (s `2 ))] ) holds
b1 = b2
proof end;
existence
ex b1 being Function of the carrier of (CatSign the Objects of C1),the carrier of (CatSign the Objects of C2) st
for s being SortSymbol of (CatSign the Objects of C1) holds b1 . s = [0,((Obj F) * (s `2 ))]
proof end;
func Psi F -> Function of the OperSymbols of (CatSign the Objects of C1),the OperSymbols of (CatSign the Objects of C2) means :Def14: :: CATALG_1:def 14
for o being OperSymbol of (CatSign the Objects of C1) holds it . o = [(o `1 ),((Obj F) * (o `2 ))];
uniqueness
for b1, b2 being Function of the OperSymbols of (CatSign the Objects of C1),the OperSymbols of (CatSign the Objects of C2) st ( for o being OperSymbol of (CatSign the Objects of C1) holds b1 . o = [(o `1 ),((Obj F) * (o `2 ))] ) & ( for o being OperSymbol of (CatSign the Objects of C1) holds b2 . o = [(o `1 ),((Obj F) * (o `2 ))] ) holds
b1 = b2
proof end;
existence
ex b1 being Function of the OperSymbols of (CatSign the Objects of C1),the OperSymbols of (CatSign the Objects of C2) st
for o being OperSymbol of (CatSign the Objects of C1) holds b1 . o = [(o `1 ),((Obj F) * (o `2 ))]
proof end;
end;

:: deftheorem Def13 defines Upsilon CATALG_1:def 13 :
for C1, C2 being Category
for F being Functor of C1,C2
for b4 being Function of the carrier of (CatSign the Objects of C1),the carrier of (CatSign the Objects of C2) holds
( b4 = Upsilon F iff for s being SortSymbol of (CatSign the Objects of C1) holds b4 . s = [0,((Obj F) * (s `2 ))] );

:: deftheorem Def14 defines Psi CATALG_1:def 14 :
for C1, C2 being Category
for F being Functor of C1,C2
for b4 being Function of the OperSymbols of (CatSign the Objects of C1),the OperSymbols of (CatSign the Objects of C2) holds
( b4 = Psi F iff for o being OperSymbol of (CatSign the Objects of C1) holds b4 . o = [(o `1 ),((Obj F) * (o `2 ))] );

Lm2: now
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:56, ZFMISC_1:37;
then A1: dom (f * <*x*>) = dom <*x*> by RELAT_1:46
.= Seg 1 by FINSEQ_1:55 ;
then reconsider p = f * <*x*> as FinSequence by FINSEQ_1:def 2;
( 1 in {1} & <*x*> . 1 = x ) by FINSEQ_1:57, TARSKI:def 1;
then ( len p = 1 & p . 1 = f . x ) by A1, FINSEQ_1:4, FINSEQ_1:def 3, FUNCT_1:22;
hence f * <*x*> = <*(f . x)*> by FINSEQ_1:57; :: thesis: verum
end;

theorem Th30: :: CATALG_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th31: :: CATALG_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th32: :: CATALG_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th33: :: CATALG_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being Category
for F being Functor of C1,C2 holds Upsilon F, Psi F form_morphism_between CatSign the Objects of C1, CatSign the Objects of C2
proof end;

theorem Th34: :: CATALG_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for A being MSAlgebra of CatSign C
for a being Element of C holds Args (idsym a),A = {{} }
proof end;

Lm3: for C being Category
for A being MSAlgebra of CatSign the Objects 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{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , F4( set , set , set , set , set ) -> set , F5( set ) -> set } :
ex A being strict MSAlgebra of CatSign F1() st
( ( for a, b being Element of F1() holds the Sorts of A . (homsym a,b) = F3(a,b) ) & ( for a being Element of F1() holds (Den (idsym a),A) . {} = F5(a) ) & ( for a, b, c being Element of F1()
for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds
(Den (compsym a,b,c),A) . <*g,f*> = F4(a,b,c,g,f) ) )
provided
A1: for a, b being Element of F1() holds F3(a,b) c= F2() and
A2: for a being Element of F1() holds F5(a) in F3(a,a) and
A3: for a, b, c being Element of F1()
for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds
F4(a,b,c,g,f) in F3(a,c)
proof end;

definition
let C be Category;
func MSAlg C -> strict MSAlgebra of CatSign the Objects of C means :Def15: :: CATALG_1:def 15
( ( 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 b1, b2 being strict MSAlgebra of CatSign the Objects of C st ( for a, b being Object of C holds the Sorts of b1 . (homsym a,b) = Hom a,b ) & ( for a being Object of C holds (Den (idsym a),b1) . {} = 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),b1) . <*g,f*> = g * f ) & ( for a, b being Object of C holds the Sorts of b2 . (homsym a,b) = Hom a,b ) & ( for a being Object of C holds (Den (idsym a),b2) . {} = 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),b2) . <*g,f*> = g * f ) holds
b1 = b2
proof end;
correctness
existence
ex b1 being strict MSAlgebra of CatSign the Objects of C st
( ( for a, b being Object of C holds the Sorts of b1 . (homsym a,b) = Hom a,b ) & ( for a being Object of C holds (Den (idsym a),b1) . {} = 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),b1) . <*g,f*> = g * f ) )
;
proof end;
end;

:: deftheorem Def15 defines MSAlg CATALG_1:def 15 :
for C being Category
for b2 being strict MSAlgebra of CatSign the Objects of C holds
( b2 = MSAlg C iff ( ( for a, b being Object of C holds the Sorts of b2 . (homsym a,b) = Hom a,b ) & ( for a being Object of C holds (Den (idsym a),b2) . {} = 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),b2) . <*g,f*> = g * f ) ) );

theorem :: CATALG_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th36: :: CATALG_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Category
for a being Object of A holds Result (idsym a),(MSAlg A) = Hom a,a
proof end;

theorem Th37: :: CATALG_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

registration
let C be Category;
cluster MSAlg C -> strict feasible disjoint_valued ;
coherence
( MSAlg C is disjoint_valued & MSAlg C is feasible )
proof end;
end;

theorem Th38: :: CATALG_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being Category
for F being Functor of C1,C2 holds F -MSF the carrier of (CatSign the Objects of C1),the Sorts of (MSAlg C1) is ManySortedFunction of (MSAlg C1),((MSAlg C2) | (CatSign the Objects of C1),(Upsilon F),(Psi F))
proof end;

theorem Th39: :: CATALG_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th40: :: CATALG_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Objects of C1),(Upsilon F),(Psi F)) st H = F -MSF the carrier of (CatSign the Objects of C1),the Sorts of (MSAlg C1) holds
H # x = <*(F . g),(F . f)*>
proof end;

theorem :: CATALG_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th42: :: CATALG_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: CATALG_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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*>
proof end;

theorem :: CATALG_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: CATALG_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being Category
for F being Functor of C1,C2 ex H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | (CatSign the Objects of C1),(Upsilon F),(Psi F)) st
( H = F -MSF the carrier of (CatSign the Objects of C1),the Sorts of (MSAlg C1) & H is_homomorphism MSAlg C1,(MSAlg C2) | (CatSign the Objects of C1),(Upsilon F),(Psi F) )
proof end;