:: Examples of Category Structures
:: by Adam Grabowski
::
:: Received June 11, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, STRUCT_0, MSUALG_1, ALTCAT_1, MSALIMIT, SUBSET_1,
FUNCT_1, CAT_1, RELAT_1, PBOOLE, ZFMISC_1, MCART_1, PUA2MSS1, RELAT_2,
BINOP_1, TARSKI, MSUALG_6, FUNCT_2, PARTFUN1, NUMBERS, CARD_3, FUNCOP_1,
PZFMISC1, MARGREL1, MEMBER_1, FUNCT_6, FINSEQ_4, MSUALG_3, MSINST_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XTUPLE_0,
MCART_1, RELAT_1, FUNCT_1, STRUCT_0, FUNCT_2, RELSET_1, PARTFUN1,
FINSEQ_2, CARD_3, BINOP_1, MULTOP_1, FUNCT_6, FUNCOP_1, PBOOLE, PZFMISC1,
PRALG_1, MSUALG_1, MSUALG_3, ALTCAT_1, PRALG_2, PUA2MSS1, MSUALG_6,
MSALIMIT;
constructors PZFMISC1, MSUALG_3, ALTCAT_1, PUA2MSS1, CLOSURE1, MSUALG_6,
MSALIMIT, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCOP_1, RELAT_1,
STRUCT_0, MSUALG_1, ALTCAT_1, MSUALG_6, MSALIMIT, MSSUBFAM, PBOOLE,
FINSEQ_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions ALTCAT_1, MSUALG_3, PBOOLE, TARSKI;
equalities ALTCAT_1, TARSKI, BINOP_1;
expansions MSUALG_3, TARSKI;
theorems XBOOLE_0, ALTCAT_1, ALTCAT_2, AUTALG_1, CARD_3, CLOSURE1, FUNCOP_1,
FUNCT_1, FUNCT_2, FUNCT_6, FUNCTOR0, MCART_1, MSSUBFAM, MSUALG_1,
MSUALG_3, MSUALG_6, MSALIMIT, MULTOP_1, PARTFUN1, PBOOLE, PRALG_2,
PUA2MSS1, RELAT_1, TARSKI, ZFMISC_1, PRALG_1, XBOOLE_1, PZFMISC1,
FINSEQ_2, XTUPLE_0;
schemes ALTCAT_1, MSSUBFAM, TARSKI, XBOOLE_0;
begin :: Category of Many Sorted Signatures
reserve A for non empty set,
S for non void non empty ManySortedSign;
reserve x for set;
definition
let A;
func MSSCat A -> strict non empty AltCatStr means
:Def1:
the carrier of it =
MSS_set A & ( for i, j be Element of MSS_set A holds (the Arrows of it).(i,j) =
MSS_morph (i,j) ) & for i,j,k be Object of it st i in MSS_set A & j in MSS_set
A & k in MSS_set A for f1,f2,g1,g2 be 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
set c = MSS_set A;
deffunc F((Element of c),Element of c) = MSS_morph ($1,$2);
consider M be ManySortedSet of [:c,c:] such that
A1: for i,j be Element of c holds M.(i,j) = F(i,j) from ALTCAT_1:sch 2;
defpred P[object,object,object] means
ex i,j,k be Element of MSS_set A st $3 = [i,j
,k] & for f1,f2,g1,g2 be Function st [f1,f2] in M.(i,j) & [g1,g2] in M.(j,k) &
$2 = [[g1,g2],[f1,f2]] holds $1 = [g1*f1,g2*f2];
A2: for ijk be object st ijk in [:c,c,c:]
for x be object st x in {|M,M|}.
ijk ex y be object st y in {|M|}.ijk & P[y,x,ijk]
proof
let ijk be object;
assume ijk in [:c,c,c:];
then consider x1,x2,x3 be object such that
A3: x1 in c & x2 in c & x3 in c and
A4: ijk = [x1,x2,x3] by MCART_1:68;
reconsider x1,x2,x3 as Element of c by A3;
let x be object;
A5: {|M,M|}.(x1,x2,x3) = {|M,M|}.[x1,x2,x3] & {|M,M|}.(x1,x2,x3) = [:M.(
x2,x3),M .(x1,x2):] by ALTCAT_1:def 4,MULTOP_1:def 1;
A6: {|M|}.ijk = {|M|}.(x1,x2,x3) by A4,MULTOP_1:def 1;
assume
A7: x in {|M,M|}.ijk;
then x`1 in M.(x2,x3) by A4,A5,MCART_1:10;
then x`1 in MSS_morph (x2,x3) by A1;
then consider g1,g2 be Function such that
A8: x`1 = [g1,g2] and
A9: g1,g2 form_morphism_between x2,x3 by MSALIMIT:def 10;
x`2 in M.(x1,x2) by A4,A7,A5,MCART_1:10;
then x`2 in MSS_morph (x1,x2) by A1;
then consider f1,f2 be Function such that
A10: x`2 = [f1,f2] and
A11: f1,f2 form_morphism_between x1,x2 by MSALIMIT:def 10;
take y = [g1*f1,g2*f2];
g1*f1, g2*f2 form_morphism_between x1,x3 by A11,A9,PUA2MSS1:29;
then {|M|}.(x1,x2,x3) = M.(x1,x3) & y in MSS_morph (x1,x3) by
ALTCAT_1:def 3,MSALIMIT:def 10;
hence y in {|M|}.ijk by A1,A6;
take x1,x2,x3;
thus ijk = [x1,x2,x3] by A4;
let F1,F2,G1,G2 be Function;
assume that
[F1,F2] in M.(x1,x2) and
[G1,G2] in M.(x2,x3) and
A12: x = [[G1,G2],[F1,F2]];
x`1 = [G1,G2] by A12;
then
A13: G1 = g1 & G2 = g2 by A8,XTUPLE_0:1;
A14: x`2 = [F1,F2] by A12;
then F1 = f1 by A10,XTUPLE_0:1;
hence thesis by A10,A14,A13,XTUPLE_0:1;
end;
consider F be ManySortedFunction of {|M,M|}, {|M|} such that
A15: for ijk be object st ijk in [:c,c,c:] holds ex f be Function of {|M,
M|}.ijk, {|M|}.ijk st f = F.ijk &
for x be object st x in {|M,M|}.ijk holds P[f.x,
x,ijk] from MSSUBFAM:sch 1 (A2);
take EX = AltCatStr (#c,M,F#);
reconsider EX as non empty AltCatStr;
for i,j,k be Object of EX st i in MSS_set A & j in MSS_set A & k in
MSS_set A for f1,f2,g1,g2 be Function st [f1,f2] in (the Arrows of EX).(i,j) &
[g1,g2] in (the Arrows of EX).(j,k) holds (the Comp of EX).(i,j,k).([g1,g2],[f1
,f2]) = [g1*f1,g2*f2]
proof
let i,j,k be Object of EX;
assume that
i in MSS_set A and
j in MSS_set A and
k in MSS_set A;
let f1,f2,g1,g2 be Function;
assume
A16: [f1,f2] in (the Arrows of EX).(i,j) & [g1,g2] in (the Arrows of
EX).(j,k);
set x = [[g1,g2],[f1,f2]];
set ijk = [i,j,k];
ijk in [:c,c,c:] by MCART_1:69;
then consider f be Function of {|M,M|}.ijk, {|M|}.ijk such that
A17: f = F.ijk and
A18: for x be object st x in {|M,M|}.ijk holds P[f.x,x,ijk] by A15;
A19: f = (the Comp of EX).(i,j,k) by A17,MULTOP_1:def 1;
{|M,M|}.(i,j,k) = {|M,M|}.[i,j,k] & {|M,M|}.(i,j,k) = [:M.(j,k),M.(
i,j):] by ALTCAT_1:def 4,MULTOP_1:def 1;
then x in {|M,M|}.ijk by A16,ZFMISC_1:87;
then consider I,J,K be Element of MSS_set A such that
A20: ijk = [I,J,K] and
A21: for f1,f2,g1,g2 be Function st [f1,f2] in M.(I,J) & [g1,g2] in
M.(J,K) & x = [[g1,g2],[f1,f2]] holds f.x = [g1*f1,g2*f2] by A18;
A22: K = k by A20,XTUPLE_0:3;
I = i & J = j by A20,XTUPLE_0:3;
hence thesis by A16,A21,A22,A19;
end;
hence thesis by A1;
end;
uniqueness
proof
set c = MSS_set A;
let A1, A2 be non empty strict AltCatStr such that
A23: the carrier of A1 = MSS_set A and
A24: for i, j be Element of MSS_set A holds (the Arrows of A1).(i,j) =
MSS_morph (i,j) and
A25: for i,j,k be Object of A1 st i in MSS_set A & j in MSS_set A & k
in MSS_set A for f1,f2,g1,g2 be Function st [f1,f2] in (the Arrows of A1).(i,j)
& [g1,g2] in (the Arrows of A1).(j,k) holds (the Comp of A1).(i,j,k).([g1,g2],[
f1,f2]) = [g1*f1,g2*f2] and
A26: the carrier of A2 = MSS_set A and
A27: for i, j be Element of MSS_set A holds (the Arrows of A2).(i,j) =
MSS_morph (i,j) and
A28: for i,j,k be Object of A2 st i in MSS_set A & j in MSS_set A & k
in MSS_set A for f1,f2,g1,g2 be Function st [f1,f2] in (the Arrows of A2).(i,j)
& [g1,g2] in (the Arrows of A2).(j,k) holds (the Comp of A2).(i,j,k).([g1,g2],[
f1,f2]) = [g1*f1,g2*f2];
reconsider AA2 = the Arrows of A2 as ManySortedSet of [:c, c:] by A26;
reconsider AA1 = the Arrows of A1 as ManySortedSet of [:c, c:] by A23;
reconsider CC1 = (the Comp of A1), CC2 = the Comp of A2 as ManySortedSet
of [:c,c,c:] by A23,A26;
A29: now
let i, j be Element of MSS_set A;
thus AA1.(i,j) = MSS_morph (i,j) by A24
.= AA2.(i,j) by A27;
end;
then
A30: AA1 = AA2 by ALTCAT_1:7;
now
let i,j,k be object;
set ijk = [i,j,k];
A31: CC1.(i,j,k) = CC1.[i,j,k] by MULTOP_1:def 1;
assume
A32: i in MSS_set A & j in MSS_set A & k in MSS_set A;
then reconsider i9=i,j9=j,k9=k as Element of c;
reconsider I9 = i,J9 = j,K9 = k as Element of A2 by A26,A32;
reconsider I = i,J = j,K = k as Element of A1 by A23,A32;
A33: ijk in [:c,c,c:] by A32,MCART_1:69;
A34: CC2.(i,j,k) = CC2.[i,j,k] by MULTOP_1:def 1;
thus CC1.(i,j,k) = CC2.(i,j,k)
proof
reconsider Cj = CC2.ijk as Function of {|AA2,AA2|}.ijk, {|AA2|}.ijk by
A26,A33,PBOOLE:def 15;
reconsider Ci = CC1.ijk as Function of {|AA1,AA1|}.ijk, {|AA1|}.ijk by
A23,A33,PBOOLE:def 15;
per cases;
suppose
A35: {|AA1|}.ijk <> {};
A36: for x be object st x in {|AA1,AA1|}.ijk holds Ci.x = Cj.x
proof
let x be object;
assume
A37: x in {|AA1,AA1|}.ijk;
then x in {|AA1,AA1|}.(i,j,k) by MULTOP_1:def 1;
then
A38: x in [:AA1.(j,k),AA1.(i,j):] by A32,ALTCAT_1:def 4;
then
A39: x`1 in AA1.(j,k) by MCART_1:10;
then x`1 in MSS_morph (j9,k9) by A24;
then consider g1,g2 be Function such that
A40: x `1 = [g1,g2] and
g1,g2 form_morphism_between j9,k9 by MSALIMIT:def 10;
x in {|AA2,AA2|}.(i,j,k) by A30,A37,MULTOP_1:def 1;
then x in [:AA2.(j,k), AA2.(i,j):] by A32,ALTCAT_1:def 4;
then
A41: x`1 in AA2.( j,k) & x`2 in AA2.(i,j) by MCART_1:10;
A42: x`2 in AA1.(i,j) by A38,MCART_1:10;
then x`2 in MSS_morph (i9,j9 ) by A24;
then consider f1,f2 be Function such that
A43: x`2 = [f1,f2] and
f1,f2 form_morphism_between i9,j9 by MSALIMIT:def 10;
A44: x = [[g1,g2],[f1,f2]] by A38,A40,A43,MCART_1:21;
then Ci.x = (the Comp of A1).(I,J,K).([g1,g2],[f1,f2]) by
MULTOP_1:def 1
.= [g1*f1,g2*f2] by A23,A25,A39,A42,A40,A43
.= (the Comp of A2).(I9,J9,K9).([g1,g2],[f1,f2]) by A26,A28,A41
,A40,A43
.= Cj.x by A44,MULTOP_1:def 1;
hence thesis;
end;
{|AA2|}.ijk <> {} by A29,A35,ALTCAT_1:7;
then
A45: dom Cj = {|AA2,AA2|}.ijk by FUNCT_2:def 1;
dom Ci = {|AA1,AA1|}.ijk by A35,FUNCT_2:def 1;
hence thesis by A30,A31,A34,A45,A36,FUNCT_1:2;
end;
suppose
{|AA1|}.ijk = {};
then Ci = {} & Cj = {} by A30;
hence thesis by A31,MULTOP_1:def 1;
end;
end;
end;
hence thesis by A23,A26,A30,ALTCAT_1:8;
end;
end;
registration
let A;
cluster MSSCat A -> transitive associative with_units;
coherence
proof
set M = MSSCat A;
set G = MSSCat A;
thus G is transitive
proof
let o1,o2,o3 be Object of G;
reconsider o19=o1, o29=o2,o39=o3 as Element of MSS_set A by Def1;
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {};
set s = the Element of MSS_morph (o29,o39);
MSS_morph (o29,o39) <> {} by A2,Def1;
then consider u,w be Function such that
s = [u,w] and
A3: u,w form_morphism_between o29,o39 by MSALIMIT:def 10;
set t = the Element of MSS_morph (o19,o29);
MSS_morph (o19,o29) <> {} by A1,Def1;
then consider f,g be Function such that
t = [f,g] and
A4: f,g form_morphism_between o19,o29 by MSALIMIT:def 10;
u * f, w * g form_morphism_between o19,o39 by A4,A3,PUA2MSS1:29;
then [u * f, w * g] in MSS_morph (o19,o39) by MSALIMIT:def 10;
hence thesis by Def1;
end;
set G = the Arrows of M, C = the Comp of M;
thus C is associative
proof
let i,j,k,l be Element of M;
reconsider I=i,J=j,K=k,L=l as Object of M;
let f,g,h be set;
reconsider i9=i,j9=j,k9=k,l9=l as Element of MSS_set A by Def1;
assume that
A5: f in G.(i,j) and
A6: g in G.(j,k) and
A7: h in G.(k,l);
g in MSS_morph (j9,k9) by A6,Def1;
then consider g1,g2 be Function such that
A8: g = [g1,g2] and
A9: g1,g2 form_morphism_between j9,k9 by MSALIMIT:def 10;
f in MSS_morph (i9,j9) by A5,Def1;
then consider f1,f2 be Function such that
A10: f = [f1,f2] and
A11: f1,f2 form_morphism_between i9,j9 by MSALIMIT:def 10;
A12: C.(i,j,k).(g,f) = [g1*f1,g2*f2] by A5,A6,A10,A11,A8,A9,Def1;
h in MSS_morph (k9,l9) by A7,Def1;
then consider h1,h2 be Function such that
A13: h = [h1,h2] and
A14: h1,h2 form_morphism_between k9,l9 by MSALIMIT:def 10;
A15: C.(j,k,l).(h,g) = [h1*g1,h2*g2] by A6,A7,A8,A9,A13,A14,Def1;
h1*g1,h2*g2 form_morphism_between j9,l9 by A9,A14,PUA2MSS1:29;
then [h1*g1,h2*g2] in MSS_morph (j9,l9) by MSALIMIT:def 10;
then
A16: [h1*g1,h2*g2] in G.(j,l) by Def1;
A17: h1*g1*f1 = h1*(g1*f1) & h2*g2*f2 = h2*(g2*f2) by RELAT_1:36;
J in the carrier of M;
then
A18: J in MSS_set A by Def1;
L in the carrier of M;
then
A19: L in MSS_set A by Def1;
g1*f1,g2*f2 form_morphism_between i9,k9 by A11,A9,PUA2MSS1:29;
then [g1*f1,g2*f2] in MSS_morph (i9,k9) by MSALIMIT:def 10;
then
A20: [g1*f1,g2*f2] in G.(i,k) by Def1;
I in the carrier of M;
then
A21: I in MSS_set A by Def1;
K in the carrier of M;
then K in MSS_set A by Def1;
then C.(i,k,l).(h,[g1*f1,g2*f2]) = [h1*(g1*f1),h2*(g2*f2)] by A21,A19,A7
,A13,A20,Def1;
hence thesis by A21,A18,A19,A5,A10,A12,A15,A16,A17,Def1;
end;
thus C is with_left_units
proof
let j be Element of M;
reconsider j9 = j as Element of MSS_set A by Def1;
set e1 = id the carrier of j9,e2 = id the carrier' of j9;
reconsider e = [e1,e2] as set;
take e;
e1, e2 form_morphism_between j9,j9 & G.(j,j) = MSS_morph (j9,j9) by Def1,
PUA2MSS1:28;
hence
A22: e in G.(j,j) by MSALIMIT:def 10;
let i be Element of M;
reconsider i9 = i as Element of MSS_set A by Def1;
let f be set;
reconsider I=i,J=j as Object of M;
assume
A23: f in G.(i,j);
then f in MSS_morph (i9,j9) by Def1;
then consider f1,f2 be Function such that
A24: f = [f1,f2] and
A25: f1,f2 form_morphism_between i9,j9 by MSALIMIT:def 10;
A26: rng f2 c= the carrier' of j9 by A25,PUA2MSS1:def 12;
rng f1 c= the carrier of j9 by A25,PUA2MSS1:def 12;
then
A27: e1*f1 = f1 by RELAT_1:53;
C.(I,J,J).([e1,e2],[f1,f2]) = [e1*f1,e2*f2] by A22,A23,A24,A25,Def1;
hence thesis by A24,A26,A27,RELAT_1:53;
end;
thus C is with_right_units
proof
let i be Element of M;
reconsider i9 = i as Element of MSS_set A by Def1;
set e1 = id the carrier of i9,e2 = id the carrier' of i9;
reconsider e = [e1,e2] as set;
take e;
e1, e2 form_morphism_between i9,i9 & G.(i,i) = MSS_morph (i9,i9) by Def1,
PUA2MSS1:28;
hence
A28: e in G.(i,i) by MSALIMIT:def 10;
let j be Element of M;
reconsider j9 = j as Element of MSS_set A by Def1;
let f be set;
reconsider I=i,J=j as Object of M;
assume
A29: f in G.(i,j);
then f in MSS_morph (i9,j9) by Def1;
then consider f1,f2 be Function such that
A30: f = [f1,f2] and
A31: f1,f2 form_morphism_between i9,j9 by MSALIMIT:def 10;
A32: dom f2 = the carrier' of i9 by A31,PUA2MSS1:def 12;
dom f1 = the carrier of i9 by A31,PUA2MSS1:def 12;
then
A33: f1*e1 = f1 by RELAT_1:52;
C.(I,I,J).([f1,f2],[e1,e2]) = [f1*e1,f2*e2] by A28,A29,A30,A31,Def1;
hence thesis by A30,A32,A33,RELAT_1:52;
end;
end;
end;
theorem
for C be category st C = MSSCat A for o be Object of C holds o is non
empty non void ManySortedSign
proof
let C be category;
assume
A1: C = MSSCat A;
let o be Object of C;
reconsider o as Element of MSS_set A by A1,Def1;
o is non empty non void ManySortedSign;
hence thesis;
end;
registration
let S;
cluster strict feasible for MSAlgebra over S;
existence
proof
set M = the feasible MSAlgebra over S;
take E = the MSAlgebra of M;
thus E is strict;
now
let o be OperSymbol of S;
A1: Args (o,M) = ((the Sorts of E)# * the Arity of S).o by MSUALG_1:def 4
.= Args (o,E) by MSUALG_1:def 4;
Result (o,M) = ((the Sorts of E) * the ResultSort of S).o by
MSUALG_1:def 5
.= Result (o,E) by MSUALG_1:def 5;
hence Args(o,E) <> {} implies Result(o,E) <> {} by A1,MSUALG_6:def 1;
end;
hence thesis by MSUALG_6:def 1;
end;
end;
definition
let S, A;
func MSAlg_set (S,A) -> set means
:Def2:
for x being object holds
x in it iff ex M be strict feasible MSAlgebra over S st x = M &
for C be Component of the Sorts of M holds C c= A;
existence
proof
defpred P[object,object] means
ex M be strict feasible MSAlgebra over S st M = $2 &
$1 = [the Sorts of M, the Charact of M ];
A1: for x,y,z be object st P[x,y] & P[x,z] holds y = z
proof
let x,y,z be object;
given M be strict feasible MSAlgebra over S such that
A2: M = y and
A3: x = [the Sorts of M, the Charact of M ];
given N be strict feasible MSAlgebra over S such that
A4: N = z and
A5: x = [the Sorts of N, the Charact of N ];
the Sorts of M = the Sorts of N by A3,A5,XTUPLE_0:1;
hence thesis by A2,A3,A4,A5,XTUPLE_0:1;
end;
consider X be set such that
A6: for x being object holds x in X iff
ex y be object st y in [:Funcs (the carrier of S, bool A)
, Funcs (the carrier' of S,PFuncs(PFuncs (NAT ,A),A)):] & P[y,x]
from TARSKI: sch 1 (A1);
take X;
thus for x being object holds
x in X iff ex M be strict feasible MSAlgebra over S st x = M & for C
be Component of the Sorts of M holds C c= A
proof let x be object;
hereby
assume x in X;
then consider y be object such that
A7: y in [:Funcs (the carrier of S, bool A) , Funcs (the carrier'
of S, PFuncs (PFuncs (NAT,A),A)):] and
A8: P[y,x] by A6;
consider M be strict feasible MSAlgebra over S such that
A9: M = x and
y = [the Sorts of M, the Charact of M ] by A8;
take M;
thus x = M by A9;
thus for C be Component of the Sorts of M holds C c= A
proof
let C be Component of the Sorts of M;
consider y1 be object such that
y1 in dom the Sorts of M and
A10: C = (the Sorts of M).y1 by FUNCT_1:def 3;
the Sorts of M in Funcs (the carrier of S, bool A) by A7,A8,A9,
ZFMISC_1:87;
then consider f be Function such that
A11: the Sorts of M = f and
dom f = the carrier of S and
A12: rng f c= bool A by FUNCT_2:def 2;
f.y1 in rng f by A10,A11;
hence thesis by A10,A11,A12;
end;
end;
given M be strict feasible MSAlgebra over S such that
A13: x = M and
A14: for C be Component of the Sorts of M holds C c= A;
A15: dom the Sorts of M = the carrier of S by PARTFUN1:def 2;
then reconsider
SM = the Sorts of M as Function of the carrier of S, rng the
Sorts of M by FUNCT_2:1;
A16: rng the Sorts of M c= bool A
proof
let x be object;
assume x in rng the Sorts of M;
then reconsider x9 = x as Component of the Sorts of M;
x9 c= A by A14;
hence thesis;
end;
then reconsider SM9 = SM as Function of the carrier of S, bool A by
FUNCT_2:6;
consider y be set such that
A17: y = [the Sorts of M, the Charact of M];
A18: dom the Charact of M = the carrier' of S by PARTFUN1:def 2;
rng the Charact of M c= PFuncs(PFuncs (NAT,A),A)
proof
reconsider SA = (the Sorts of M)# * the Arity of S, SR = (the Sorts of
M) * the ResultSort of S as ManySortedSet of the carrier' of S;
let x be object;
reconsider CM = the Charact of M as ManySortedFunction of SA,SR;
assume x in rng the Charact of M;
then consider x1 be object such that
A19: x1 in dom the Charact of M and
A20: x = (the Charact of M).x1 by FUNCT_1:def 3;
reconsider Cm = CM.x1 as Function of SA.x1, SR.x1 by A19,PBOOLE:def 15;
A21: x1 in dom SA by A18,A19,PARTFUN1:def 2;
SA.x1 c= PFuncs (NAT ,A)
proof
reconsider AX = (the Arity of S).x1 as Element of (the carrier of S)
* by A19,FUNCT_2:5;
let a be object;
assume a in SA.x1;
then
A22: a in ((the Sorts of M)# ).((the Arity of S).x1) by A21,FUNCT_1:12;
((the Sorts of M)# ).AX = product ( (the Sorts of M) * AX) by
FINSEQ_2:def 5;
then
A23: ex g be Function st a = g & dom g = dom ( (the Sorts of M ) * AX
) & for x2 be object st x2 in dom ((the Sorts of M) * AX)
holds g.x2 in (( the
Sorts of M) * AX).x2 by A22,CARD_3:def 5;
then reconsider a9=a as Function;
rng AX c= dom the Sorts of M by A15;
then
A24: dom a9 = dom AX by A23,RELAT_1:27;
rng a9 c= A
proof
rng the Sorts of M c= bool A
proof
let w be object;
assume w in rng the Sorts of M;
then reconsider w9=w as Component of the Sorts of M;
w9 c= A by A14;
hence thesis;
end;
then
A25: union rng the Sorts of M c= union bool A by ZFMISC_1:77;
let r be object;
assume r in rng a9;
then consider r1 be object such that
A26: r1 in dom a9 and
A27: r = a9.r1 by FUNCT_1:def 3;
AX.r1 in rng AX by A24,A26,FUNCT_1:def 3;
then
A28: (the Sorts of M).(AX.r1) in rng the Sorts of M by A15,FUNCT_1:def 3
;
r in ((the Sorts of M) * AX).r1 by A23,A26,A27;
then r in (the Sorts of M).(AX.r1) by A24,A26,FUNCT_1:13;
then r in union rng the Sorts of M by A28,TARSKI:def 4;
then r in union bool A by A25;
hence thesis by ZFMISC_1:81;
end;
hence thesis by A23,PARTFUN1:def 3;
end;
then
A29: dom Cm c= PFuncs(NAT,A);
x1 in dom SR by A18,A19,PARTFUN1:def 2;
then
A30: SR.x1 = (the Sorts of M).((the ResultSort of S).x1) by FUNCT_1:12;
(the ResultSort of S).x1 in the carrier of S by A19,FUNCT_2:5;
then SR.x1 in rng (the Sorts of M) by A15,A30,FUNCT_1:def 3;
then rng Cm c= A by A16,XBOOLE_1:1;
hence thesis by A20,A29,PARTFUN1:def 3;
end;
then
SM9 in Funcs (the carrier of S, bool A) & the Charact of M in Funcs
(the carrier' of S,PFuncs(PFuncs (NAT ,A),A)) by A18,FUNCT_2:8,def 2;
then
y in [:Funcs (the carrier of S, bool A) , Funcs (the carrier' of S,
PFuncs(PFuncs (NAT ,A),A)):] by A17,ZFMISC_1:87;
hence thesis by A6,A13,A17;
end;
end;
uniqueness
proof
let A1, A2 be set;
assume
A31: for x being object holds
x in A1 iff ex M be strict feasible MSAlgebra over S st x = M &
for C be Component of the Sorts of M holds C c= A;
assume
A32: for x being object holds
x in A2 iff ex N be strict feasible MSAlgebra over S st x = N &
for C be Component of the Sorts of N holds C c= A;
A33: A2 c= A1
proof
let a be object;
assume a in A2;
then ex M be strict feasible MSAlgebra over S st a = M & for C be
Component of the Sorts of M holds C c= A by A32;
hence thesis by A31;
end;
A1 c= A2
proof
let a be object;
assume a in A1;
then ex M be strict feasible MSAlgebra over S st a = M & for C be
Component of the Sorts of M holds C c= A by A31;
hence thesis by A32;
end;
hence A1 = A2 by A33,XBOOLE_0:def 10;
end;
end;
registration
let S, A;
cluster MSAlg_set (S,A) -> non empty;
coherence
proof
set a = the Element of A;
reconsider
f = (the carrier of S) --> {a} as ManySortedSet of the carrier
of S;
set Ch = the ManySortedFunction of f# * the Arity of S, f * the ResultSort of S
;
set Ex = MSAlgebra(#f,Ch#);
reconsider Ex as non-empty MSAlgebra over S by MSUALG_1:def 3;
reconsider Ex as strict feasible MSAlgebra over S;
for C be Component of the Sorts of Ex holds C c= A
proof
let C be Component of the Sorts of Ex;
ex i be object st i in the carrier of S & C = (the Sorts of Ex).i by
PBOOLE:138;
then C = {a} by FUNCOP_1:7;
hence thesis by ZFMISC_1:31;
end;
hence thesis by Def2;
end;
end;
begin :: Category of Many Sorted Algebras
reserve o for OperSymbol of S;
theorem
for x be MSAlgebra over 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
carrier' of S,PFuncs(PFuncs (NAT ,A),A))
proof
let x be MSAlgebra over S;
assume x in MSAlg_set (S,A);
then consider M be strict feasible MSAlgebra over S such that
A1: x = M and
A2: for C be Component of the Sorts of M holds C c= A by Def2;
A3: dom the Sorts of M = the carrier of S by PARTFUN1:def 2;
then reconsider SM = the Sorts of M as Function of the carrier of S, rng the
Sorts of M by FUNCT_2:1;
A4: rng the Sorts of M c= bool A
proof
let x be object;
assume x in rng the Sorts of M;
then reconsider x9 = x as Component of the Sorts of M;
x9 c= A by A2;
hence thesis;
end;
then reconsider SM9 = SM as Function of the carrier of S, bool A by FUNCT_2:6
;
A5: dom the Charact of M = the carrier' of S by PARTFUN1:def 2;
A6: rng the Charact of M c= PFuncs(PFuncs (NAT,A),A)
proof
reconsider SA = (the Sorts of M)# * the Arity of S, SR = (the Sorts of M)
* the ResultSort of S as ManySortedSet of the carrier' of S;
let x be object;
reconsider CM = the Charact of M as ManySortedFunction of SA,SR;
assume x in rng the Charact of M;
then consider x1 be object such that
A7: x1 in dom the Charact of M and
A8: x = (the Charact of M).x1 by FUNCT_1:def 3;
reconsider Cm = CM.x1 as Function of SA.x1, SR.x1 by A7,PBOOLE:def 15;
A9: x1 in dom SA by A5,A7,PARTFUN1:def 2;
SA.x1 c= PFuncs (NAT ,A)
proof
reconsider AX = (the Arity of S).x1 as Element of (the carrier of S)*
by A7,FUNCT_2:5;
let a be object;
assume a in SA.x1;
then
A10: a in ((the Sorts of M)# ).((the Arity of S).x1) by A9,FUNCT_1:12;
((the Sorts of M)# ).AX = product ( (the Sorts of M) * AX) by
FINSEQ_2:def 5;
then
A11: ex g be Function st a = g & dom g = dom ( (the Sorts of M ) * AX) &
for x2 be object st x2 in dom ((the Sorts of M) * AX)
holds g.x2 in (( the Sorts
of M) * AX).x2 by A10,CARD_3:def 5;
then reconsider a9=a as Function;
rng AX c= dom the Sorts of M by A3;
then
A12: dom a9 = dom AX by A11,RELAT_1:27;
rng a9 c= A
proof
rng the Sorts of M c= bool A
proof
let w be object;
assume w in rng the Sorts of M;
then reconsider w9=w as Component of the Sorts of M;
w9 c= A by A2;
hence thesis;
end;
then
A13: union rng the Sorts of M c= union bool A by ZFMISC_1:77;
let r be object;
assume r in rng a9;
then consider r1 be object such that
A14: r1 in dom a9 and
A15: r = a9.r1 by FUNCT_1:def 3;
AX.r1 in rng AX by A12,A14,FUNCT_1:def 3;
then
A16: (the Sorts of M).(AX.r1) in rng the Sorts of M by A3,FUNCT_1:def 3;
r in ((the Sorts of M) * AX).r1 by A11,A14,A15;
then r in (the Sorts of M).(AX.r1) by A12,A14,FUNCT_1:13;
then r in union rng the Sorts of M by A16,TARSKI:def 4;
then r in union bool A by A13;
hence thesis by ZFMISC_1:81;
end;
hence thesis by A11,PARTFUN1:def 3;
end;
then
A17: dom Cm c= PFuncs(NAT,A);
x1 in dom SR by A5,A7,PARTFUN1:def 2;
then
A18: SR.x1 = (the Sorts of M).((the ResultSort of S).x1) by FUNCT_1:12;
(the ResultSort of S).x1 in the carrier of S by A7,FUNCT_2:5;
then SR.x1 in rng (the Sorts of M) by A3,A18,FUNCT_1:def 3;
then rng Cm c= A by A4,XBOOLE_1:1;
hence thesis by A8,A17,PARTFUN1:def 3;
end;
SM9 in Funcs (the carrier of S, bool A) by FUNCT_2:8;
hence thesis by A1,A5,A6,FUNCT_2:def 2;
end;
theorem Th3:
for U1,U2 be MSAlgebra over S st the Sorts of U1
is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds Args (o,U2) <> {}
proof
let U1,U2 be MSAlgebra over S;
assume that
A1: the Sorts of U1 is_transformable_to the Sorts of U2 and
A2: Args (o,U1) <> {};
A3: ((the Sorts of U1)# * the Arity of S).o <> {} by A2,MSUALG_1:def 4;
dom (the Sorts of U1) = the carrier of S by PARTFUN1:def 2;
then rng (the_arity_of o) c= dom (the Sorts of U1);
then
A4: dom ((the Sorts of U1) * (the_arity_of o)) = dom (the_arity_of o) by
RELAT_1:27;
A5: dom ((the Sorts of U2) * (the_arity_of o)) c= dom (the_arity_of o) by
RELAT_1:25;
A6: dom (the Arity of S) = the carrier' of S by FUNCT_2:def 1;
then ((the Sorts of U1)# * the Arity of S).o = (the Sorts of U1)# . ((the
Arity of S).o) by FUNCT_1:13
.= (the Sorts of U1)# . (the_arity_of o) by MSUALG_1:def 1;
then product ((the Sorts of U1) * (the_arity_of o)) <> {} by A3,
FINSEQ_2:def 5;
then
A7: not {} in rng ((the Sorts of U1) * (the_arity_of o)) by CARD_3:26;
now
let x be object;
assume
A8: x in dom ((the Sorts of U2) * ( the_arity_of o ) );
then (the_arity_of o).x in rng (the_arity_of o) by A5,FUNCT_1:def 3;
then
A9: (the Sorts of U1).((the_arity_of o).x) <> {} implies (the Sorts of U2
).((the_arity_of o).x) <> {} by A1,PZFMISC1:def 3;
((the Sorts of U1) * (the_arity_of o)).x = (the Sorts of U1).((
the_arity_of o).x) by A5,A8,FUNCT_1:13;
hence ((the Sorts of U2)*(the_arity_of o)).x <> {} by A7,A4,A5,A8,A9,
FUNCT_1:13,def 3;
end;
then not {} in rng ((the Sorts of U2) * (the_arity_of o)) by FUNCT_1:def 3;
then product ((the Sorts of U2)*(the_arity_of o)) <> {} by CARD_3:26;
then (the Sorts of U2)# . (the_arity_of o) <> {} by FINSEQ_2:def 5;
then (the Sorts of U2)# . ((the Arity of S).o) <> {} by MSUALG_1:def 1;
then ((the Sorts of U2)# * the Arity of S).o <> {} by A6,FUNCT_1:13;
hence thesis by MSUALG_1:def 4;
end;
theorem Th4:
for U1,U2,U3 be feasible MSAlgebra over S,
F be ManySortedFunction of U1,U2,
G be ManySortedFunction of U2,U3,
x be 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
ex GF be ManySortedFunction of U1,U3 st GF = G ** F & GF#x = G#(F#x)
proof
let U1,U2,U3 be feasible MSAlgebra over S, F be ManySortedFunction of U1,U2,
G be ManySortedFunction of U2,U3, x be Element of Args(o,U1);
assume that
A1: Args (o,U1) <> {} and
A2: the Sorts of U1 is_transformable_to the Sorts of U2 and
A3: the Sorts of U2 is_transformable_to the Sorts of U3;
x in Args (o,U1) by A1;
then x in product ((the Sorts of U1)*(the_arity_of o)) by PRALG_2:3;
then
A4: ex g be Function st x = g & dom g = dom ((the Sorts of U1 )*(the_arity_of
o)) & for x being object st x in dom ((the Sorts of U1)*(the_arity_of o))
holds g.x in ((the
Sorts of U1)*(the_arity_of o)).x by CARD_3:def 5;
then reconsider x9 = x as Function;
reconsider Fr = (Frege (F*the_arity_of o)).x9 as Function;
dom F = the carrier of S by PARTFUN1:def 2;
then
A5: rng the_arity_of o c= dom F; then
A6: dom (F*the_arity_of o) = dom the_arity_of o by RELAT_1:27;
A7: dom doms (F*the_arity_of o) = dom (F*the_arity_of o) by FUNCT_6:59;
then
A8: dom x9 = dom doms (F*the_arity_of o) by A1,A6,MSUALG_3:6;
then reconsider
x99 = x9 as ManySortedSet of dom (the_arity_of o) by A6,A7,PARTFUN1:def 2
,RELAT_1:def 18;
dom G = the carrier of S by PARTFUN1:def 2;
then rng the_arity_of o c= dom G;
then
A9: dom (G*the_arity_of o) = dom the_arity_of o by RELAT_1:27;
then reconsider Ga = (G*the_arity_of o), Fa = (F*the_arity_of o) as
ManySortedFunction of dom (the_arity_of o) by A6,PARTFUN1:def 2
,RELAT_1:def 18;
A10: Args (o,U2) <> {} by A1,A2,Th3;
dom (the Sorts of U1) = the carrier of S by PARTFUN1:def 2;
then
A11: rng the_arity_of o c= dom the Sorts of U1;
now
let x be object;
set ds = (the_arity_of o).x;
assume x in dom doms (F*the_arity_of o); then
A12: x in dom (F*the_arity_of o) by FUNCT_6:59;
then
A13: (doms (F*the_arity_of o)).x = dom ((F*the_arity_of o).x) by FUNCT_6:22;
A14: x in dom the_arity_of o by A5,A12,RELAT_1:27; then
A15: ds in rng the_arity_of o by FUNCT_1:def 3;
then reconsider
Ff = F.ds as Function of (the Sorts of U1).ds, (the Sorts of U2
).ds by PBOOLE:def 15;
x in dom ((the Sorts of U1) * (the_arity_of o)) by A11,A14,RELAT_1:27;
then
A16: x9.x in ((the Sorts of U1) * (the_arity_of o)).x by A1,MSUALG_3:6;
A17: (the Sorts of U1).ds = dom Ff
proof
per cases;
suppose
(the Sorts of U2).ds <> {};
hence thesis by FUNCT_2:def 1;
end;
suppose
(the Sorts of U2).ds = {};
then (the Sorts of U1).ds = {} by A2,A15,PZFMISC1:def 3;
hence thesis;
end;
end;
((F*the_arity_of o).x) = F.((the_arity_of o).x) by A14,FUNCT_1:13;
hence x9.x in (doms (F*the_arity_of o)).x by A13,A14,A16,A17,FUNCT_1:13;
end; then
A18: x9 in product doms (F*the_arity_of o) by A8,CARD_3:9; then
A19: Fr = (F*the_arity_of o)..x9 by PRALG_2:def 2;
A20: now
let x be object;
set ds = (the_arity_of o).x;
assume
A21: x in dom doms (G*the_arity_of o); then
A22: x in dom (G*the_arity_of o) by FUNCT_6:59;
Z2: dom x9 = dom the_arity_of o by A1,MSUALG_3:6;
Z1: x in dom (F*the_arity_of o) by A9,A6,A21,FUNCT_6:59;
Z3: dom (F*the_arity_of o) = dom the_arity_of o by A6; then
dom (F*the_arity_of o) /\ dom x9 = dom the_arity_of o by Z2; then
x in dom (F*the_arity_of o) /\ dom x9 by Z1,Z3; then
x in dom ((F*the_arity_of o)..x9) by PRALG_1:def 19; then
A23: Fr.x = ((F*the_arity_of o).x).(x9.x) by A19,PRALG_1:def 19;
A24: dom ((the Sorts of U1) * (the_arity_of o)) = dom (the_arity_of o)
by A11,RELAT_1:27;
A25: x in dom the_arity_of o by A9,A21,FUNCT_6:59; then
A26: ds in rng the_arity_of o by FUNCT_1:def 3;
then reconsider
Ff = F.ds as Function of (the Sorts of U1).ds, (the Sorts of U2).ds
by PBOOLE:def 15;
A27: ((F*the_arity_of o).x) = Ff by A6,A25,FUNCT_1:12;
reconsider Gds = G.ds as Function of (the Sorts of U2).ds, (the Sorts of
U3).ds by A26,PBOOLE:def 15;
A28: dom Gds = (the Sorts of U2).ds
proof
per cases;
suppose
(the Sorts of U3).ds <> {};
hence thesis by FUNCT_2:def 1;
end;
suppose
(the Sorts of U3).ds = {};
then (the Sorts of U2).ds = {} by A3,A26,PZFMISC1:def 3;
hence thesis;
end;
end;
A29: (the Sorts of U1).ds = dom Ff
proof
per cases;
suppose
(the Sorts of U2).ds <> {};
hence thesis by FUNCT_2:def 1;
end;
suppose
(the Sorts of U2).ds = {};
then (the Sorts of U1).ds = {} by A2,A26,PZFMISC1:def 3;
hence thesis;
end;
end;
((the Sorts of U1) * (the_arity_of o)).x = (the Sorts of U1).((
the_arity_of o).x) by A25,FUNCT_1:13;
then (x9.x) in dom Ff by A1,A25,A24,A29,MSUALG_3:6; then
A30: ((F*the_arity_of o).x).(x9.x) in rng Ff by A27,FUNCT_1:def 3;
((G*the_arity_of o).x) = G.((the_arity_of o).x) by A25,FUNCT_1:13;
then Fr.x in dom ((G*the_arity_of o).x) by A28,A30,A23;
hence Fr.x in (doms (G*the_arity_of o)).x by A22,FUNCT_6:22;
end;
reconsider GF = G ** F as ManySortedFunction of U1,U3 by A2,ALTCAT_2:4;
dom GF = the carrier of S by PARTFUN1:def 2;
then rng the_arity_of o c= dom GF; then
A31: dom (GF*the_arity_of o) = dom the_arity_of o by RELAT_1:27;
A32: x99 in doms Fa
proof
let i be object;
set ai = (the_arity_of o).i;
assume
A33: i in dom the_arity_of o; then
A34: ai in rng the_arity_of o by FUNCT_1:def 3;
Fa.i = F.((the_arity_of o).i) by A33,FUNCT_1:13;
then reconsider
Ew = Fa.i as Function of (the Sorts of U1).ai,(the Sorts of U2)
.ai by A34,PBOOLE:def 15;
A35: dom Ew = (the Sorts of U1).ai
proof
per cases;
suppose
(the Sorts of U2).ai = {};
then (the Sorts of U1).ai = {} by A2,A34,PZFMISC1:def 3;
hence thesis;
end;
suppose
(the Sorts of U2).ai <> {};
hence thesis by FUNCT_2:def 1;
end;
end;
i in dom ((the Sorts of U1)*(the_arity_of o)) by A33,PRALG_2:3;
then x99.i in ((the Sorts of U1)*(the_arity_of o)).i by A4;
then x99.i in dom (Fa.i) by A33,A35,FUNCT_1:13;
hence thesis by A33,MSSUBFAM:14;
end;
take GF;
thus GF = G ** F;
A36: (G*the_arity_of o)**(F*the_arity_of o) = GF*the_arity_of o by FUNCTOR0:12;
A37: the Sorts of U1 is_transformable_to the Sorts of U3 by A2,A3,AUTALG_1:10;
set tao = the_arity_of o;
A38: now
let x be object;
set ds = tao.x;
assume
A39: x in dom doms (GF*tao); then
A40: x in dom tao by A31,FUNCT_6:59; then
A41: ds in rng tao by FUNCT_1:def 3;
then reconsider
Gf = GF.ds as Function of (the Sorts of U1).ds, (the Sorts of U3).ds
by PBOOLE:def 15;
x in dom (GF*tao) by A39,FUNCT_6:59; then
A42: (doms (GF*tao)).x = dom ((GF*tao).x) by FUNCT_6:22;
A43: (the Sorts of U1).ds = dom Gf
proof
per cases;
suppose
(the Sorts of U3).ds <> {};
hence thesis by FUNCT_2:def 1;
end;
suppose
(the Sorts of U3).ds = {};
then (the Sorts of U1).ds = {} by A37,A41,PZFMISC1:def 3;
hence thesis;
end;
end;
x in dom ((the Sorts of U1) * tao) by A11,A40,RELAT_1:27;
then x9.x in ((the Sorts of U1) * tao).x by A1,MSUALG_3:6;
then x9.x in dom (GF.ds) by A40,A43,FUNCT_1:13;
hence x9.x in (doms (GF*tao)).x by A42,A40,FUNCT_1:13;
end;
dom doms (GF*tao) = dom (GF*tao) by FUNCT_6:59;
then dom x9 = dom doms (GF*tao) by A1,A31,MSUALG_3:6; then
A44: x9 in product doms (GF*tao) by A38,CARD_3:9;
rng tao c= dom F by A5; then
S2: dom (F*tao) = dom tao by RELAT_1:27;
S0: dom tao = dom x99 by A1,MSUALG_3:6;
dom Fr = dom (F*tao) /\ dom x99 by A19,PRALG_1:def 19
.= dom (G*tao) by A9,S0,S2;
then dom Fr = dom doms (G*tao) by FUNCT_6:59;
then Fr in product doms (G*tao) by A20,CARD_3:9; then
A45: (Frege (G*tao)).((Frege(F*tao)).x) = (G*tao)..((Frege(F*tao)).x)
by PRALG_2:def 2
.= Ga..(Fa..x99) by A18,PRALG_2:def 2
.= (Ga**Fa)..x99 by A32,CLOSURE1:4;
A46: Args (o,U3) <> {} by A1,A2,A3,Th3,AUTALG_1:10;
then GF#x = (Frege(GF*tao)).x by A1,MSUALG_3:def 5
.= (Frege (G*tao)).((Frege(F*tao)).x)
by A44,A45,A36,PRALG_2:def 2
.= (Frege (G*tao)).(F#x) by A1,A10,MSUALG_3:def 5;
hence thesis by A10,A46,MSUALG_3:def 5;
end;
theorem Th5:
for U1,U2,U3 be feasible MSAlgebra over S,
F be ManySortedFunction of U1,U2,
G be 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
ex GF be ManySortedFunction of U1,U3 st
GF = G ** F & GF is_homomorphism U1,U3
proof
let U1,U2,U3 be feasible MSAlgebra over S, F be ManySortedFunction of U1,U2,
G be ManySortedFunction of U2,U3;
assume that
A1: the Sorts of U1 is_transformable_to the Sorts of U2 and
A2: the Sorts of U2 is_transformable_to the Sorts of U3 and
A3: F is_homomorphism U1,U2 and
A4: G is_homomorphism U2,U3;
reconsider GF = G ** F as ManySortedFunction of U1,U3 by A1,ALTCAT_2:4;
take GF;
thus GF = G ** F;
thus GF is_homomorphism U1,U3
proof
let o be OperSymbol of S such that
A5: Args(o,U1) <> {};
let x be Element of Args(o,U1);
A6: ex gf be ManySortedFunction of U1,U3 st gf = G ** F & gf #x = G#(F#x)
by A1,A2,A5,Th4;
set r = the_result_sort_of o;
(F.r).(Den(o,U1).x) = Den(o,U2).(F#x) & Args (o,U2) <> {} by A1,A3,A5,Th3;
then
A7: (G.r).((F.r).(Den(o,U1).x)) = Den(o,U3).(G#(F#x)) by A4;
A8: the Sorts of U1 is_transformable_to the Sorts of U3 by A1,A2,AUTALG_1:10;
A9: dom (GF.r) = (the Sorts of U1).r
proof
per cases;
suppose
(the Sorts of U1).r <> {};
then (the Sorts of U3).r <> {} by A8,PZFMISC1:def 3;
hence thesis by FUNCT_2:def 1;
end;
suppose
(the Sorts of U1).r = {};
hence thesis;
end;
end;
o in the carrier' of S;
then
A10: o in dom (the ResultSort of S) by FUNCT_2:def 1;
rng (the ResultSort of S) c= the carrier of S;
then rng (the ResultSort of S) c= dom (the Sorts of U1) by PARTFUN1:def 2;
then Result(o,U1) = ((the Sorts of U1)*(the ResultSort of S)).o & dom ((
the Sorts of U1)*(the ResultSort of S)) = dom (the ResultSort of S) by
MSUALG_1:def 5,RELAT_1:27;
then
A11: Result(o,U1) = (the Sorts of U1).((the ResultSort of S).o) by A10,
FUNCT_1:12
.= (the Sorts of U1).r by MSUALG_1:def 2;
then GF.r = (G.r)*(F.r) & (the Sorts of U1).r <> {} by A5,MSUALG_3:2
,MSUALG_6:def 1;
hence thesis by A5,A7,A9,A11,A6,FUNCT_1:12,FUNCT_2:5;
end;
end;
definition
let S, A;
let i,j be set;
assume that
A1: i in MSAlg_set (S,A) and
A2: j in MSAlg_set (S,A);
func MSAlg_morph (S,A,i,j) -> set means
:Def3: x in it iff
ex M,N be strict feasible MSAlgebra over S,
f be 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
consider M being strict feasible MSAlgebra over S such that
A3: i = M and
A4: for C be Component of the Sorts of M holds C c= A by A1,Def2;
consider N being strict feasible MSAlgebra over S such that
A5: j = N and
A6: for C be Component of the Sorts of N holds C c= A by A2,Def2;
defpred P[object] means
the Sorts of M is_transformable_to the Sorts of N &
ex f being ManySortedFunction of M,N st $1 = f &
f is_homomorphism M,N;
consider X being set such that
A7: for x being object holds x in X iff
x in Funcs(the carrier of S, PFuncs (union bool A, union bool A)) &
P[x] from XBOOLE_0:sch 1;
take X; let x;
hereby
assume
A8: x in X;
then consider f being ManySortedFunction of M,N such that
A9: x = f and
A10: f is_homomorphism M,N by A7;
take M,N;
reconsider f as ManySortedFunction of M,N;
take f;
thus M = i & N = j & f = x by A3,A5,A9;
thus the Sorts of M is_transformable_to the Sorts of N by A8,A7;
thus f is_homomorphism M,N by A10;
end;
given M1,N1 be strict feasible MSAlgebra over S,
f be ManySortedFunction of M1,N1 such that
A11: M1 = i & N1 = j &
f = x & the Sorts of M1 is_transformable_to the Sorts of N1 &
f is_homomorphism M1,N1;
reconsider F = f as ManySortedFunction of M,N by A11,A3,A5;
A12: dom F = the carrier of S by PARTFUN1:def 2;
rng F c= PFuncs (union bool A, union bool A)
proof
A13: rng the Sorts of M c= bool A
proof
let x be object;
assume x in rng the Sorts of M;
then reconsider x9 = x as Component of the Sorts of M;
x9 c= A by A4;
hence thesis;
end;
let w be object;
assume w in rng F;
then consider w1 be object such that
A14: w1 in dom F and
A15: w = F.w1 by FUNCT_1:def 3;
reconsider w9 = w as Function of (the Sorts of M).w1, (the Sorts of N)
.w1 by A14,A15,PBOOLE:def 15;
A16: dom (the Sorts of M) = the carrier of S by PARTFUN1:def 2;
A17: dom w9 c= union bool A
proof
let s be object;
assume
A18: s in dom w9;
(the Sorts of M).w1 in rng (the Sorts of M) by A14,A16,FUNCT_1:def 3;
hence thesis by A13,A18,TARSKI:def 4;
end;
A19: rng the Sorts of N c= bool A
proof
let x be object;
assume x in rng the Sorts of N;
then reconsider x9 = x as Component of the Sorts of N;
x9 c= A by A6;
hence thesis;
end;
A20: dom (the Sorts of N) = the carrier of S by PARTFUN1:def 2;
rng w9 c= union bool A
proof
let r be object;
assume
A21: r in rng w9;
(the Sorts of N).w1 in rng (the Sorts of N) by A14,A20,FUNCT_1:def 3;
hence thesis by A19,A21,TARSKI:def 4;
end;
hence thesis by A17,PARTFUN1:def 3;
end;
then
F in Funcs (the carrier of S, PFuncs (union bool A, union bool A))
by A12,FUNCT_2:def 2;
hence x in X by A7,A11,A3,A5;
end;
uniqueness
proof
let A1,A2 be set;
assume
A22: x in A1 iff ex M,N be strict feasible MSAlgebra over S, f be
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;
assume
A23: x in A2 iff ex M,N be strict feasible MSAlgebra over S, f be
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;
A24: A2 c= A1
proof
let a be object;
assume a in A2;
then ex M,N be strict feasible MSAlgebra over S, f be ManySortedFunction
of M,N st M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts
of N & f is_homomorphism M,N by A23;
hence thesis by A22;
end;
A1 c= A2
proof
let a be object;
assume a in A1;
then ex M,N be strict feasible MSAlgebra over S, f be ManySortedFunction
of M,N st M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts
of N & f is_homomorphism M,N by A22;
hence thesis by A23;
end;
hence A1 = A2 by A24,XBOOLE_0:def 10;
end;
end;
definition
let S, A;
func MSAlgCat (S,A) -> strict non empty AltCatStr means :Def4:
the carrier of it = MSAlg_set (S,A) &
(for i, j be Element of MSAlg_set (S,A) holds
(the Arrows of it).(i,j) = MSAlg_morph (S,A,i,j)) &
for i,j,k be Object of it, f,g be 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
set c = MSAlg_set (S,A);
deffunc F((Element of c),Element of c) = MSAlg_morph (S,A,$1,$2);
consider M be ManySortedSet of [:c,c:] such that
A1: for i,j be Element of c holds M.(i,j) = F(i,j) from ALTCAT_1:sch 2;
defpred P[object,object,object] means
ex i,j,k be Element of c st $3 = [i,j,k] &
for f,g be Function-yielding Function st
f in M.(i,j) & g in M.(j,k) & $2 = [g,f] holds $1 = g ** f;
A2: for ijk be object st ijk in [:c,c,c:]
for x be object st x in {|M,M|}.
ijk ex y be object st y in {|M|}.ijk & P[y,x,ijk]
proof
let ijk be object;
assume ijk in [:c,c,c:];
then consider x1,x2,x3 be object such that
A3: x1 in c & x2 in c & x3 in c and
A4: ijk = [x1,x2,x3] by MCART_1:68;
reconsider x1,x2,x3 as Element of c by A3;
let x be object;
A5: {|M,M|}.(x1,x2,x3) = {|M,M|}.[x1,x2,x3] & {|M,M|}.(x1,x2,x3) = [:M.(
x2,x3),M .(x1,x2):] by ALTCAT_1:def 4,MULTOP_1:def 1;
A6: {|M|}.ijk = {|M|}.(x1,x2,x3) by A4,MULTOP_1:def 1;
assume
A7: x in {|M,M|}.ijk;
then x`1 in M.(x2,x3) by A4,A5,MCART_1:10;
then x`1 in MSAlg_morph (S,A,x2,x3) by A1;
then consider M2,N2 be strict feasible MSAlgebra over S, g be
ManySortedFunction of M2,N2 such that
A8: M2 = x2 and
A9: N2 = x3 and
A10: g = x`1 and
A11: the Sorts of M2 is_transformable_to the Sorts of N2 & g
is_homomorphism M2, N2 by Def3;
x`2 in M.(x1,x2) by A4,A7,A5,MCART_1:10;
then x`2 in MSAlg_morph (S,A,x1,x2 ) by A1;
then consider M1,N1 be strict feasible MSAlgebra over S, f be
ManySortedFunction of M1,N1 such that
A12: M1 = x1 and
A13: N1 = x2 and
A14: f = x`2 and
A15: the Sorts of M1 is_transformable_to the Sorts of N1 & f
is_homomorphism M1, N1 by Def3;
take y = g ** f;
reconsider f as ManySortedFunction of M1,M2 by A8,A13;
the Sorts of M1 is_transformable_to the Sorts of N2 & ex fg be
ManySortedFunction of M1,N2 st fg = g ** f & fg is_homomorphism M1,N2 by A8,A11
,A13,A15,Th5,AUTALG_1:10;
then
{|M|}.(x1,x2,x3) = M.(x1,x3) & y in MSAlg_morph (S,A,x1,x3) by A9,A12
,Def3,ALTCAT_1:def 3;
hence y in {|M|}. ijk by A1,A6;
take x1,x2,x3;
thus ijk = [x1,x2,x3] by A4;
let F,G be Function-yielding Function;
assume that
F in M.(x1,x2) and
G in M.(x2,x3) and
A16: x = [G,F];
thus thesis by A10,A14,A16;
end;
consider F be ManySortedFunction of {|M,M|}, {|M|} such that
A17: for ijk be object st ijk in [:c,c,c:] holds ex f be Function of {|M,
M|}.ijk, {|M|}.ijk st f = F.ijk &
for x be object st x in {|M,M|}.ijk holds P[f.x,
x,ijk] from MSSUBFAM:sch 1 (A2);
take EX = AltCatStr(#c,M,F#);
reconsider EX as non empty AltCatStr;
for i,j,k be Object of EX, f,g be Function-yielding Function st f in
(the Arrows of EX).(i,j) & g in (the Arrows of EX).(j,k) holds (the Comp of EX)
.(i,j,k).(g,f) = ( g ** f )
proof
let i,j,k be Object of EX, f,g be Function-yielding Function;
assume
A18: f in (the Arrows of EX).(i,j) & g in (the Arrows of EX).(j,k);
set x = [g,f];
set ijk = [i,j,k];
ijk in [:c,c,c:] by MCART_1:69;
then consider ff be Function of {|M,M|}.ijk, {|M|}.ijk such that
A19: ff = F.ijk and
A20: for x be object st x in {|M,M|}.ijk holds P[ff.x,x,ijk] by A17;
A21: ff = (the Comp of EX).(i,j,k) by A19,MULTOP_1:def 1;
{|M,M|}.(i,j,k) = {|M,M|}.[i,j,k] & {|M,M|}.(i,j,k) = [:M.(j,k),M.(
i,j):] by ALTCAT_1:def 4,MULTOP_1:def 1;
then x in {|M,M|}.ijk by A18,ZFMISC_1:87;
then consider I,J,K be Element of c such that
A22: ijk = [I,J,K] and
A23: for f,g be Function-yielding Function st f in M.(I,J) & g in M.
(J,K ) & x = [g,f] holds ff.x = (g ** f) by A20;
A24: K = k by A22,XTUPLE_0:3;
I = i & J = j by A22,XTUPLE_0:3;
hence thesis by A18,A23,A24,A21;
end;
hence thesis by A1;
end;
uniqueness
proof
reconsider c = MSAlg_set (S,A) as non empty set;
let A1, A2 be non empty strict AltCatStr such that
A25: the carrier of A1 = MSAlg_set (S,A) and
A26: for i, j be Element of MSAlg_set (S,A) holds (the Arrows of A1).(
i,j) = MSAlg_morph (S,A,i,j) and
A27: for i,j,k be Object of A1, f,g be Function-yielding Function st f
in (the Arrows of A1).(i,j) & g in (the Arrows of A1).(j,k) holds (the Comp of
A1).(i,j,k).(g,f) = ( g ** f ) and
A28: the carrier of A2 = MSAlg_set (S,A) and
A29: for i, j be Element of MSAlg_set (S,A) holds (the Arrows of A2).(
i,j) = MSAlg_morph (S,A,i,j) and
A30: for i,j,k be Object of A2, f,g be Function-yielding Function st f
in (the Arrows of A2).(i,j) & g in (the Arrows of A2).(j,k) holds (the Comp of
A2).(i,j,k).(g,f) = ( g ** f );
reconsider CC1 = (the Comp of A1), CC2 = the Comp of A2 as ManySortedSet
of [:c,c,c:] by A25,A28;
reconsider AA1 = the Arrows of A1, AA2 = the Arrows of A2 as ManySortedSet
of [:c, c:] by A25,A28;
A31: now
let i, j be Element of c;
thus AA1.(i,j) = MSAlg_morph (S,A,i,j) by A26
.= AA2.(i,j) by A29;
end;
then
A32: AA1 = AA2 by ALTCAT_1:7;
now
let i,j,k be object;
set ijk = [i,j,k];
A33: CC1.(i,j,k) = CC1.[i,j,k] by MULTOP_1:def 1;
assume
A34: i in c & j in c & k in c;
then reconsider i9=i,j9=j,k9=k as Element of c;
reconsider I9 = i,J9 = j,K9 = k as Object of A2 by A28,A34;
reconsider I = i,J = j,K = k as Object of A1 by A25,A34;
A35: ijk in [:c,c,c:] by A34,MCART_1:69;
A36: CC2.(i,j,k) = CC2.[i,j,k] by MULTOP_1:def 1;
thus CC1.(i,j,k) = CC2.(i,j,k)
proof
reconsider Cj = CC2.ijk as Function of {|AA2,AA2|}.ijk, {|AA2|}.ijk by
A28,A35,PBOOLE:def 15;
reconsider Ci = CC1.ijk as Function of {|AA1,AA1|}.ijk, {|AA1|}.ijk by
A25,A35,PBOOLE:def 15;
per cases;
suppose
A37: {|AA1|}.ijk <> {};
A38: for x be object st x in {|AA1,AA1|}.ijk holds Ci.x = Cj.x
proof
let x be object;
assume
A39: x in {|AA1,AA1|}.ijk;
then x in {|AA1,AA1|}.(i,j,k) by MULTOP_1:def 1;
then
A40: x in [:AA1.(j,k),AA1.(i,j):] by A34,ALTCAT_1:def 4;
then
A41: x`1 in AA1.(j,k) by MCART_1:10;
then x`1 in MSAlg_morph (S,A,j9,k9) by A26;
then consider M2,N2 be strict feasible MSAlgebra over S, g be
ManySortedFunction of M2,N2 such that
M2 = j9 and
N2 = k9 and
A42: g = x`1 and
the Sorts of M2 is_transformable_to the Sorts of N2 and
g is_homomorphism M2,N2 by Def3;
x in {|AA2,AA2|}.(i,j,k) by A32,A39,MULTOP_1:def 1;
then x in [:AA2.(j,k), AA2.(i,j):] by A34,ALTCAT_1:def 4;
then
A43: x`1 in AA2.( j,k) & x`2 in AA2.(i,j) by MCART_1:10;
A44: x`2 in AA1.(i,j) by A40,MCART_1:10;
then x`2 in MSAlg_morph (S,A,i9,j9) by A26;
then consider M1,N1 be strict feasible MSAlgebra over S, f be
ManySortedFunction of M1,N1 such that
M1 = i9 and
N1 = j9 and
A45: f = x`2 and
the Sorts of M1 is_transformable_to the Sorts of N1 and
f is_homomorphism M1,N1 by Def3;
A46: x = [g,f] by A40,A45,A42,MCART_1:21;
then Ci.x = (the Comp of A1).(I,J,K).(g,f) by MULTOP_1:def 1
.= g ** f by A27,A41,A44,A45,A42
.= (the Comp of A2).(I9,J9,K9).(g,f) by A30,A43,A45,A42
.= Cj.x by A46,MULTOP_1:def 1;
hence thesis;
end;
{|AA2|}.ijk <> {} by A31,A37,ALTCAT_1:7;
then
A47: dom Cj = {|AA2,AA2|}.ijk by FUNCT_2:def 1;
dom Ci = {|AA1,AA1|}.ijk by A37,FUNCT_2:def 1;
hence thesis by A32,A33,A36,A47,A38,FUNCT_1:2;
end;
suppose
{|AA1|}.ijk = {};
then Ci = {} & Cj = {} by A32;
hence thesis by A33,MULTOP_1:def 1;
end;
end;
end;
hence thesis by A25,A28,A32,ALTCAT_1:8;
end;
end;
registration
let S, A;
cluster MSAlgCat (S,A) -> transitive associative with_units;
coherence
proof
set M = MSAlgCat (S,A);
set G = MSAlgCat (S,A);
set GM = the Arrows of M, C = the Comp of M;
thus G is transitive
proof
let o1,o2,o3 be Object of G;
reconsider o19=o1, o29=o2,o39=o3 as Element of MSAlg_set (S,A) by Def4;
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {};
set t = the Element of MSAlg_morph (S,A,o19,o29);
MSAlg_morph (S,A,o19,o29) <> {} by A1,Def4;
then consider M,N be strict feasible MSAlgebra over S, f be
ManySortedFunction of M,N such that
A3: M = o19 and
A4: N = o29 and
f = t and
A5: the Sorts of M is_transformable_to the Sorts of N and
A6: f is_homomorphism M,N by Def3;
set s = the Element of MSAlg_morph (S,A,o29,o39);
MSAlg_morph (S,A,o29,o39) <> {} by A2,Def4;
then consider M1,N1 be strict feasible MSAlgebra over S, g be
ManySortedFunction of M1,N1 such that
A7: M1 = o29 and
A8: N1 = o39 and
g = s and
A9: the Sorts of M1 is_transformable_to the Sorts of N1 and
A10: g is_homomorphism M1,N1 by Def3;
reconsider g9 = g as ManySortedFunction of N,N1 by A4,A7;
consider GF be ManySortedFunction of M,N1 such that
GF = g9 ** f and
A11: GF is_homomorphism M,N1 by A4,A5,A6,A7,A9,A10,Th5;
the Sorts of M is_transformable_to the Sorts of N1 by A4,A5,A7,A9,
AUTALG_1:10;
then GF in MSAlg_morph (S,A,o19,o39) by A3,A8,A11,Def3;
hence thesis by Def4;
end;
thus C is associative
proof
let i,j,k,l be Element of M;
let f,g,h be set;
reconsider i9=i,j9=j,k9=k,l9=l as Element of MSAlg_set (S,A) by Def4;
assume that
A12: f in GM.(i,j) and
A13: g in GM.(j,k) and
A14: h in GM.(k,l);
g in MSAlg_morph (S,A,j9,k9) by A13,Def4;
then consider M2,N2 be strict feasible MSAlgebra over S, G be
ManySortedFunction of M2,N2 such that
A15: M2 = j9 and
A16: N2 = k9 and
A17: g = G and
A18: the Sorts of M2 is_transformable_to the Sorts of N2 and
A19: G is_homomorphism M2,N2 by Def3;
h in MSAlg_morph (S,A,k9,l9) by A14,Def4;
then consider M3,N3 be strict feasible MSAlgebra over S, H be
ManySortedFunction of M3,N3 such that
A20: M3 = k9 and
A21: N3 = l9 and
A22: h = H and
A23: the Sorts of M3 is_transformable_to the Sorts of N3 and
A24: H is_homomorphism M3,N3 by Def3;
reconsider G9 = G as ManySortedFunction of M2,M3 by A16,A20;
consider HG be ManySortedFunction of M2,N3 such that
A25: HG = H ** G9 and
A26: HG is_homomorphism M2,N3 by A16,A18,A19,A20,A23,A24,Th5;
A27: C.(j,k,l).(H,G) = H ** G9 by A13,A14,A17,A22,Def4;
f in MSAlg_morph (S,A,i9,j9) by A12,Def4;
then consider M1,N1 be strict feasible MSAlgebra over S, F be
ManySortedFunction of M1,N1 such that
A28: M1 = i9 and
A29: N1 = j9 and
A30: f = F and
A31: the Sorts of M1 is_transformable_to the Sorts of N1 and
A32: F is_homomorphism M1,N1 by Def3;
A33: C.(i,j,k).(g,f) = G ** F by A12,A13,A30,A17,Def4;
consider GF be ManySortedFunction of M1,M3 such that
A34: GF = G9 ** F and
A35: GF is_homomorphism M1,M3 by A29,A31,A32,A15,A16,A18,A19,A20,Th5;
the Sorts of M1 is_transformable_to the Sorts of M3 by A29,A31,A15,A16
,A18,A20,AUTALG_1:10;
then G9 ** F in MSAlg_morph (S,A,i9,k9) by A28,A20,A34,A35,Def3;
then GF in GM.(i,k) by A34,Def4;
then
A36: C.(i,k,l).(H,GF) = H ** GF by A14,A22,Def4;
the Sorts of M2 is_transformable_to the Sorts of N3 by A16,A18,A20,A23,
AUTALG_1:10;
then HG in MSAlg_morph (S,A,j9,l9) by A15,A21,A26,Def3;
then
A37: H ** G9 in GM.(j,l) by A25,Def4;
(H ** G9) ** F = H ** (G9 ** F) by PBOOLE:140;
hence thesis by A12,A30,A17,A22,A33,A34,A36,A27,A37,Def4;
end;
thus C is with_left_units
proof
let j be Element of M;
reconsider j9 = j as Element of MSAlg_set (S,A) by Def4;
consider MS be strict feasible MSAlgebra over S such that
A38: MS = j9 and
for C be Component of the Sorts of MS holds C c= A by Def2;
reconsider e = id (the Sorts of MS) as ManySortedFunction of MS,MS;
take e;
e is_homomorphism MS,MS & GM.(j,j) = MSAlg_morph (S,A,j9,j9) by Def4,
MSUALG_3:9;
hence
A39: e in GM.(j,j) by A38,Def3;
let i be Element of M;
reconsider i9 = i as Element of MSAlg_set (S,A) by Def4;
let f be set;
reconsider I=i,J=j as Object of M;
assume
A40: f in GM.(i,j);
then f in MSAlg_morph (S,A,i9,j9) by Def4;
then consider M1,N1 be strict feasible MSAlgebra over S, F be
ManySortedFunction of M1,N1 such that
M1 = i9 and
A41: N1 = j9 and
A42: F = f and
the Sorts of M1 is_transformable_to the Sorts of N1 and
F is_homomorphism M1,N1 by Def3;
reconsider F as ManySortedFunction of M1,MS by A38,A41;
C.(I,J,J).(e,f) = e ** F by A39,A40,A42,Def4;
hence thesis by A42,MSUALG_3:4;
end;
thus C is with_right_units
proof
let i be Element of M;
reconsider i9 = i as Element of MSAlg_set (S,A) by Def4;
consider MS be strict feasible MSAlgebra over S such that
A43: MS = i9 and
for C be Component of the Sorts of MS holds C c= A by Def2;
reconsider e = id (the Sorts of MS) as ManySortedFunction of MS,MS;
take e;
e is_homomorphism MS,MS & GM.(i,i) = MSAlg_morph (S,A,i9,i9) by Def4,
MSUALG_3:9;
hence
A44: e in GM.(i,i) by A43,Def3;
let j be Element of M;
reconsider j9 = j as Element of MSAlg_set (S,A) by Def4;
let f be set;
reconsider I=i,J=j as Object of M;
assume
A45: f in GM.(i,j);
then f in MSAlg_morph (S,A,i9,j9) by Def4;
then consider M1,N1 be strict feasible MSAlgebra over S, F be
ManySortedFunction of M1,N1 such that
A46: M1 = i9 and
N1 = j9 and
A47: F = f and
the Sorts of M1 is_transformable_to the Sorts of N1 and
F is_homomorphism M1,N1 by Def3;
reconsider F as ManySortedFunction of MS,N1 by A43,A46;
C.(I,I,J).(f,e) = F ** e by A44,A45,A47,Def4;
hence thesis by A47,MSUALG_3:3;
end;
end;
end;
theorem
for C be category st C = MSAlgCat (S,A) for o be Object of C holds o
is strict feasible MSAlgebra over S
proof
let C be category such that
A1: C = MSAlgCat (S,A);
let o be Object of C;
o in the carrier of C;
then o in MSAlg_set (S,A) by A1,Def4;
then ex M be strict feasible MSAlgebra over S st o = M & for C1 be Component
of the Sorts of M holds C1 c= A by Def2;
hence thesis;
end;