:: MSINST_1 semantic presentation

definition

let A be non empty set ;
func MSSCat A -> non empty strict AltCatStr means :Def1: :: MSINST_1:def 1
( the carrier of it = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of it . i,j = MSS_morph i,j ) & ( for i, j, k being object of it st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of it . i,j & [g1,g2] in the Arrows of it . j,k holds
(the Comp of it . i,j,k) . [g1,g2],[f1,f2] = [(g1 * f1),(g2 * f2)] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines MSSCat MSINST_1:def 1 :

registration

let A be non empty set ;
cluster MSSCat A -> non empty transitive strict associative with_units ;
coherence

proof end;

end;

theorem :: MSINST_1:1

for A being non empty set
for C being category st C = MSSCat A holds
for o being object of C holds o is non empty non void ManySortedSign

proof end;

registration

let S be non empty non void ManySortedSign ;
cluster strict feasible MSAlgebra of S;
existence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let A be non empty set ;
func MSAlg_set S,A -> set means :Def2: :: MSINST_1:def 2
for x being set holds
( x in it iff ex M being strict feasible MSAlgebra of S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines MSAlg_set MSINST_1:def 2 :

registration

let S be non empty non void ManySortedSign ;
let A be non empty set ;
cluster MSAlg_set S,A -> non empty ;
coherence

proof end;

end;

theorem Th2: :: MSINST_1:2

for A being non empty set
for S being non empty non void ManySortedSign
for x being MSAlgebra of S st x in MSAlg_set S,A holds
( the Sorts of x in Funcs the carrier of S,(bool A) & the Charact of x in Funcs the OperSymbols of S,(PFuncs (PFuncs NAT ,A),A) )

proof end;

theorem Th3: :: MSINST_1:3

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2 being MSAlgebra of S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args o,U1 <> {} holds
Args o,U2 <> {}

proof end;

theorem Th4: :: MSINST_1:4

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2, U3 being feasible MSAlgebra of S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3
for x being Element of Args o,U1 st Args o,U1 <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )

proof end;

theorem Th5: :: MSINST_1:5

for S being non empty non void ManySortedSign
for U1, U2, U3 being feasible MSAlgebra of S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non empty set ;
let i, j be set ;
assume A1: ( i in MSAlg_set S,A & j in MSAlg_set S,A ) ;
func MSAlg_morph S,A,i,j -> set means :Def3: :: MSINST_1:def 3
for x being set holds
( x in it iff ex M, N being strict feasible MSAlgebra of S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines MSAlg_morph MSINST_1:def 3 :

definition

let S be non empty non void ManySortedSign ;
let A be non empty set ;
func MSAlgCat S,A -> non empty strict AltCatStr means :Def4: :: MSINST_1:def 4
( the carrier of it = MSAlg_set S,A & ( for i, j being Element of MSAlg_set S,A holds the Arrows of it . i,j = MSAlg_morph S,A,i,j ) & ( for i, j, k being object of it
for f, g being Function-yielding Function st f in the Arrows of it . i,j & g in the Arrows of it . j,k holds
(the Comp of it . i,j,k) . g,f = g ** f ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines MSAlgCat MSINST_1:def 4 :

registration

let S be non empty non void ManySortedSign ;
let A be non empty set ;
cluster MSAlgCat S,A -> non empty transitive strict associative with_units ;
coherence

proof end;

end;

theorem :: MSINST_1:6

for A being non empty set
for S being non empty non void ManySortedSign
for C being category st C = MSAlgCat S,A holds
for o being object of C holds o is strict feasible MSAlgebra of S

proof end;