### The Mizar article:

### More on Products of Many Sorted Algebras

**by****Mariusz Giero**

- Received April 29, 1996
Copyright (c) 1996 Association of Mizar Users

- MML identifier: PRALG_3
- [ MML identifier index ]

environ vocabulary PBOOLE, AMI_1, MSUALG_1, PRALG_2, EQREL_1, FUNCT_1, CARD_3, ZF_REFLE, RELAT_1, BOOLE, RLVECT_2, FUNCT_2, PRALG_1, FRAENKEL, TARSKI, QC_LANG1, UNIALG_2, FUNCT_5, CQC_LANG, FUNCT_6, TDGROUP, FINSEQ_4, FINSEQ_1, BORSUK_1, ALG_1, MSUALG_3, ARYTM_3, WELLORD1, GROUP_6, PRALG_3; notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, STRUCT_0, FUNCT_2, FRAENKEL, CQC_LANG, EQREL_1, FINSEQ_1, FUNCT_5, FUNCT_6, CARD_3, PBOOLE, MSUALG_1, MSUALG_3, PRALG_2, AMI_1, FINSEQ_4, PRALG_1, MSUALG_2; constructors EQREL_1, AMI_1, PRALG_2, FINSEQ_4, MSUALG_3, TOLER_1; clusters SUBSET_1, STRUCT_0, MSUALG_1, FUNCT_1, PBOOLE, AMI_1, PUA2MSS1, RELAT_1, MSUALG_3, PRALG_1, RELSET_1, MSAFREE, PRALG_2, FILTER_1, EQREL_1, TOLER_1, PARTFUN1; requirements NUMERALS, BOOLE, SUBSET; definitions XBOOLE_0, FUNCT_1, MSUALG_1, MSUALG_3, PRALG_2, PBOOLE, TARSKI; theorems PBOOLE, FUNCT_1, EQREL_1, PRALG_2, MSUALG_1, MSUALG_3, FUNCT_2, CARD_3, AMI_1, TARSKI, CQC_LANG, FINSEQ_4, MSUALG_2, PRALG_1, FINSEQ_1, FUNCT_6, UNIALG_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, PARTFUN1; schemes MSUALG_1, MSSUBFAM, FUNCT_1, PRALG_2; begin ::Preliminaries ::------------------------------------------------------------------- :: Acknowledgements: :: ================ :: :: I would like to thank Professor A.Trybulec for his help in the preparation :: of the article. ::------------------------------------------------------------------- reserve I for non empty set, J for ManySortedSet of I, S for non void non empty ManySortedSign, i for Element of I, c for set, A for MSAlgebra-Family of I,S, EqR for Equivalence_Relation of I, U0,U1,U2 for MSAlgebra over S, s for SortSymbol of S, o for OperSymbol of S, f for Function; definition let I be set, S; let AF be MSAlgebra-Family of I,S; cluster product AF -> non-empty; coherence proof the Sorts of product AF = SORTS AF by PRALG_2:20; hence thesis by MSUALG_1:def 8; end; end; definition let I be set; redefine func id I -> ManySortedSet of I; coherence proof dom(id I) = I by FUNCT_1:34; hence thesis by PBOOLE:def 3; end; end; definition let I, EqR; cluster Class EqR -> with_non-empty_elements; coherence by EQREL_1:42; end; definition let X be with_non-empty_elements set; redefine func id X -> non-empty ManySortedSet of X; coherence proof reconsider NE = id X as ManySortedSet of X; NE is non-empty proof let i be set; assume A1: i in X; then NE.i = i by FUNCT_1:34; hence NE.i is non empty by A1,AMI_1:def 1; end; hence thesis; end; end; theorem Th1: for f,F being Function, A being set st f in product F holds f|A in product(F|A) proof let f,F be Function, A be set; assume A1: f in product F; then dom f = dom F by CARD_3:18; then A2: dom (f|A) = dom F /\ A by RELAT_1:90 .= dom (F|A)by RELAT_1:90; for x be set st x in dom (F|A) holds (f|A).x in (F|A).x proof let x be set; assume A3: x in dom (F|A); then A4: (F|A).x = F.x by FUNCT_1:70; A5: (f|A).x = f.x by A2,A3,FUNCT_1:70; x in dom F /\ A by A3,RELAT_1:90; then x in dom F by XBOOLE_0:def 3; hence thesis by A1,A4,A5,CARD_3:18; end; hence thesis by A2,CARD_3:18; end; theorem Th2: for A be MSAlgebra-Family of I,S, s be SortSymbol of S, a be non empty Subset of I, Aa be MSAlgebra-Family of a,S st A|a = Aa holds Carrier(Aa,s) = (Carrier(A,s))|a proof let A be MSAlgebra-Family of I,S, s be SortSymbol of S, a be non empty Subset of I, Aa be MSAlgebra-Family of a,S such that A1: A|a = Aa; dom ((Carrier(A,s))|a) = dom (Carrier(A,s)) /\ a by RELAT_1:90 .= I /\ a by PBOOLE:def 3 .= a by XBOOLE_1:28; then reconsider Cas = ((Carrier(A,s))|a) as ManySortedSet of a by PBOOLE:def 3; for i be set st i in a holds (Carrier(Aa,s)).i = Cas.i proof let i be set; assume A2: i in a; then reconsider i' = i as Element of a; reconsider i'' = i' as Element of I; A3: Aa.i' = A.i' by A1,FUNCT_1:72; consider U0 being MSAlgebra over S such that A4:U0 = Aa.i & (Carrier(Aa,s)).i = (the Sorts of U0).s by A2,PRALG_2:def 16; consider U1 being MSAlgebra over S such that A5:U1 = A.i'' & (Carrier(A,s)).i'' = (the Sorts of U1).s by PRALG_2:def 16; thus thesis by A3,A4,A5,FUNCT_1:72; end; hence thesis by PBOOLE:3; end; theorem Th3: for i be set, I be non empty set, EqR be Equivalence_Relation of I, c1,c2 be Element of Class EqR st i in c1 & i in c2 holds c1 = c2 proof let i be set, I be non empty set, EqR be Equivalence_Relation of I, c1,c2 be Element of Class EqR such that A1: i in c1 and A2: i in c2; consider x1 be set such that x1 in I and A3: c1 = Class(EqR,x1) by EQREL_1:def 5; consider x2 be set such that x2 in I and A4: c2 = Class(EqR,x2) by EQREL_1:def 5; A5: [i,x1] in EqR by A1,A3,EQREL_1:27; [i,x2] in EqR by A2,A4,EQREL_1:27; then Class(EqR,x2) = Class(EqR,i) by A1,EQREL_1:44 .= c1 by A1,A3,A5,EQREL_1:44; hence thesis by A4; end; Lm1: for f be Function, x be set st x in product f holds x is Function proof let f be Function, x be set; assume x in product f; then consider g be Function such that A1: x = g & dom g = dom f & for x' be set st x' in dom f holds g.x' in f.x' by CARD_3:def 5; thus thesis by A1; end; theorem Th4: for X,Y being set for f being Function st f in Funcs(X,Y) holds dom f = X & rng f c= Y proof let X,Y be set; let f be Function; assume f in Funcs(X,Y); then consider f1 be Function such that A1: f1 = f & dom f1 = X & rng f1 c= Y by FUNCT_2:def 2; thus thesis by A1; end; theorem for D being non empty set for F being ManySortedFunction of D for C being with_common_domain functional non empty set st C = rng F for d being Element of D,e being set st d in dom F & e in DOM C holds F.d.e = (commute F).e.d proof let D be non empty set; let F be ManySortedFunction of D; let C be with_common_domain functional non empty set such that A1: C = rng F; let d be Element of D,e be set; assume A2: d in dom F & e in DOM C; set E = union { rng(F.d') where d' is Element of D : not contradiction}; reconsider F'= F as Function; A3: dom F' = D by PBOOLE:def 3; rng F' c= Funcs(DOM C,E) proof let x be set; assume x in rng F'; then consider d' be set such that A4:d' in dom F & F.d' = x by FUNCT_1:def 5; reconsider d' as Element of D by A4,PBOOLE:def 3; consider Fd be Function such that A5:Fd = F.d'; F.d' in rng F by A4,FUNCT_1:def 5; then A6: dom Fd = DOM C by A1,A5,PRALG_2:def 2; rng Fd c= E proof let x1 be set such that A7: x1 in rng Fd; rng Fd in { rng(F.d'') where d'' is Element of D : not contradiction} by A5; hence x1 in E by A7,TARSKI:def 4; end; hence x in Funcs(DOM C,E) by A4,A5,A6,FUNCT_2:def 2; end; then F in Funcs(D,Funcs(DOM C,E)) by A3,FUNCT_2:def 2; hence thesis by A2,PRALG_2:5; end; begin :: Constants of Many Sorted Algebras definition let S,U0; let o be OperSymbol of S; func const(o,U0) equals :Def1: Den(o,U0).{}; correctness; end; theorem Th6: the_arity_of o = {} & Result(o,U0) <> {} implies const(o,U0) in Result(o,U0) proof assume A1: the_arity_of o = {} & Result(o,U0) <> {}; then dom Den(o,U0) = Args(o,U0) by FUNCT_2:def 1 .= {{}} by A1,PRALG_2:11; then {} in dom Den(o,U0) by TARSKI:def 1; then Den(o,U0).{} in rng Den(o,U0) by FUNCT_1:def 5; then Den(o,U0).{} in Result(o,U0); hence const(o,U0) in Result(o,U0) by Def1; end; theorem (the Sorts of U0).s <> {} implies Constants(U0,s) = { const(o,U0) where o is Element of the OperSymbols of S : the_result_sort_of o = s & the_arity_of o = {} } proof assume A1: (the Sorts of U0).s <> {}; thus Constants(U0,s) c= { const(o,U0) where o is Element of the OperSymbols of S : the_result_sort_of o = s & the_arity_of o = {} } proof let x be set; assume A2: x in Constants(U0,s); ex A being non empty set st A =(the Sorts of U0).s & Constants(U0,s) = { a where a is Element of A : ex o be OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = s & a in rng Den(o,U0)} by A1,MSUALG_2:def 4; then consider A being non empty set such that A =(the Sorts of U0).s and A3: x in { a where a is Element of A : ex o be OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = s & a in rng Den(o,U0)} by A2; consider a be Element of A such that A4: a = x and A5: ex o be OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = s & a in rng Den(o,U0) by A3; consider o1 be OperSymbol of S such that A6: (the Arity of S).o1 = {} and A7: (the ResultSort of S).o1 = s and A8: a in rng Den(o1,U0) by A5; consider x1 be set such that A9: x1 in dom Den(o1,U0) and A10: a = Den(o1,U0).x1 by A8,FUNCT_1:def 5; A11: the_result_sort_of o1 = s by A7,MSUALG_1:def 7; A12: the_arity_of o1 = {} by A6,MSUALG_1:def 6; then Args(o1,U0) = {{}} by PRALG_2:11; then x = Den(o1,U0).{} by A4,A9,A10,TARSKI:def 1 .= const(o1,U0) by Def1; hence x in { const(o,U0) where o is Element of the OperSymbols of S : the_result_sort_of o = s & the_arity_of o = {} } by A11,A12; end; let x be set; assume x in { const(o,U0) where o is Element of the OperSymbols of S : the_result_sort_of o = s & the_arity_of o = {} }; then consider o being Element of the OperSymbols of S such that A13: x = const(o,U0) and A14: the_result_sort_of o = s and A15: the_arity_of o = {}; o in the OperSymbols of S; then A16: o in dom (the ResultSort of S) by FUNCT_2:def 1; A17: Result(o,U0) = ((the Sorts of U0) * the ResultSort of S).o by MSUALG_1:def 10 .= (the Sorts of U0).((the ResultSort of S).o) by A16,FUNCT_1:23 .= (the Sorts of U0).s by A14,MSUALG_1:def 7; thus x in Constants(U0,s) proof consider A being non empty set such that A18: A =(the Sorts of U0).s and A19: Constants(U0,s) = { a where a is Element of A : ex o be OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = s & a in rng Den(o,U0)} by A1,MSUALG_2:def 4; A20: x is Element of A by A13,A15,A17,A18,Th6; ex o be OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = s & x in rng Den(o,U0) proof take o; A21: Args(o,U0) = dom Den(o,U0) by A1,A17,FUNCT_2:def 1; Args(o,U0) = {{}} by A15,PRALG_2:11; then A22: {} in dom Den(o,U0) by A21,TARSKI:def 1; x = Den(o,U0).{} by A13,Def1; hence thesis by A14,A15,A22,FUNCT_1:def 5,MSUALG_1:def 6,def 7; end; hence x in Constants(U0,s) by A19,A20; end; end; theorem Th8: the_arity_of o = {} implies (commute (OPER A)).o in Funcs(I,Funcs({{}}, union { Result(o,A.i') where i' is Element of I: not contradiction })) proof assume A1: the_arity_of o = {}; set f = (commute (OPER A)).o; commute (OPER A) in Funcs(the OperSymbols of S, Funcs(I,rng uncurry (OPER A))) by PRALG_2:13; then consider f1 be Function such that A2: commute (OPER A) = f1 and A3:dom f1 = the OperSymbols of S and A4: rng f1 c= Funcs(I,rng uncurry (OPER A)) by FUNCT_2:def 2; f in rng commute (OPER A) by A2,A3,FUNCT_1:def 5; then consider fb be Function such that A5: fb = f & dom fb = I & rng fb c= rng uncurry (OPER A) by A2,A4,FUNCT_2:def 2; set C = union { Result(o,A.i') where i' is Element of I: not contradiction }; now let x be set such that A6: x in rng f; A7: f = A?.o by PRALG_2:def 19; consider a be set such that A8: a in dom f & f.a = x by A6,FUNCT_1:def 5; reconsider a as Element of I by A5,A8; reconsider x' = x as Function by A7,A8,PRALG_1:def 15; A9: x' = (A?.o).a by A8,PRALG_2:def 19 .= Den(o,A.a) by PRALG_2:14; then A10: dom x' = Args(o,A.a) by FUNCT_2:def 1 .= {{}} by A1,PRALG_2:11; now let c be set; assume c in rng x'; then consider b be set such that A11: b in dom x' & x'.b = c by FUNCT_1:def 5; x'.b = (Den(o,A.a)).{} by A9,A10,A11,TARSKI:def 1 .= const(o,A.a) by Def1; then A12: c is Element of Result(o,A.a) by A1,A11,Th6; Result(o,A.a) in { Result(o,A.i') where i' is Element of I: not contradiction }; hence c in C by A12,TARSKI:def 4; end; then rng x' c= C by TARSKI:def 3; hence x in Funcs({{}},C) by A10,FUNCT_2:def 2; end; then rng f c= Funcs({{}},C) by TARSKI:def 3; hence thesis by A5,FUNCT_2:def 2; end; theorem Th9: the_arity_of o = {} implies const(o,product A) in Funcs(I, union { Result(o,A.i') where i' is Element of I: not contradiction }) proof assume A1:the_arity_of o = {}; A2: (OPS A).o = (IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o))) by PRALG_2:def 20 .= commute(A?.o) by A1,CQC_LANG:def 1; set g = (commute (OPER A)).o; set C = union { Result(o,A.i') where i' is Element of I: not contradiction }; A3: g in Funcs(I,Funcs({{}},C)) by A1,Th8; reconsider g as Function; A4: const(o,product A) = Den(o,product A).{} by Def1 .= ((the Charact of product A).o).{} by MSUALG_1:def 11 .= (commute(A?.o)).{} by A2,PRALG_2:20 .= (commute g).{} by PRALG_2:def 19; A5: {} in {{}} by TARSKI:def 1; commute g in Funcs({{}},Funcs(I,C)) by A3,PRALG_2:4; then consider g1 be Function such that A6: g1 = commute g & dom g1 = {{}} & rng g1 c= Funcs(I,C) by FUNCT_2:def 2; g1.{} in rng g1 by A5,A6,FUNCT_1:def 5; hence thesis by A4,A6; end; definition let S,I,o,A; cluster const (o,product A) -> Relation-like Function-like; coherence proof const(o,product A) is Function proof per cases; suppose the_arity_of o = {}; then const(o,product A) in Funcs(I, union { Result(o,A.i') where i' is Element of I: not contradiction }) by Th9; then consider g be Function such that A1: g = const(o,product A) & dom g = I & rng g c= union { Result(o,A.i') where i' is Element of I: not contradiction } by FUNCT_2:def 2; thus thesis by A1; suppose A2:the_arity_of o <> {}; A3:dom Den(o,product A) = Args(o,product A) by FUNCT_2:def 1 .= product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:10; dom ((the Sorts of (product A))*(the_arity_of o)) = dom (the_arity_of o) by PRALG_2:10; then dom ((the Sorts of (product A))*(the_arity_of o)) <> dom {} by A2,FINSEQ_1:26; then A4: not {} in dom Den(o,product A) by A3,CARD_3:18; const(o,product A) = Den(o,product A).{} by Def1 .= {} by A4,FUNCT_1:def 4; hence thesis; end; hence thesis; end; end; theorem Th10: for o be OperSymbol of S st the_arity_of o = {} holds (const (o,product A)).i = const (o,A.i) proof let o be OperSymbol of S such that A1: the_arity_of o = {}; A2: (OPS A).o = (IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o))) by PRALG_2:def 20 .= commute(A?.o) by A1,CQC_LANG:def 1; set f = (commute (OPER A)).o, C = union { Result(o,A.i') where i' is Element of I: not contradiction }; A3: f in Funcs(I,Funcs({{}},C)) by A1,Th8; A4: const(o,product A) = Den(o,product A).{} by Def1 .= ((the Charact of product A).o).{} by MSUALG_1:def 11 .= (commute(A?.o)).{} by A2,PRALG_2:20 .= (commute f).{} by PRALG_2:def 19; consider f' be Function such that A5: f = f' and A6: dom f' = I & rng f' c= Funcs({{}},C) by A3,FUNCT_2:def 2; f'.i in rng f' by A6,FUNCT_1:def 5; then consider g be Function such that A7: f.i = g and dom g = {{}} & rng g c= C by A5,A6,FUNCT_2:def 2; A8: {} in {{}} by TARSKI:def 1; const (o,A.i) = Den(o,A.i).{} by Def1 .= ((A?.o).i).{} by PRALG_2:14 .= g.{} by A7,PRALG_2:def 19 .= const(o,product A).i by A3,A4,A7,A8,PRALG_2:5; hence thesis; end; theorem the_arity_of o = {} & dom f = I & (for i be Element of I holds f.i = const(o,A.i)) implies f = const(o,product A) proof assume that A1: the_arity_of o = {} & dom f = I and A2:for i be Element of I holds f.i = const(o,A.i); set C = union { Result(o,A.i') where i' is Element of I: not contradiction }; const(o,product A) in Funcs(I,C) by A1,Th9; then consider g2 be Function such that A3: g2 = const(o,product A) & dom g2 = I & rng g2 c= C by FUNCT_2:def 2; now let a be set; assume a in I; then reconsider a' = a as Element of I; thus f.a = const(o,A.a') by A2 .= (const(o,product A)).a by A1,Th10; end; hence f = const(o,product A) by A1,A3,FUNCT_1:9; end; theorem Th12: for e be Element of Args(o,U1) st e = {} & the_arity_of o = {} & Args(o,U1) <> {} & Args(o,U2) <> {} for F be ManySortedFunction of U1,U2 holds F#e = {} proof let e be Element of Args(o,U1) such that A1: e = {} & the_arity_of o = {} and A2: Args(o,U1) <> {} & Args(o,U2) <> {}; let F be ManySortedFunction of U1,U2; reconsider e1 = e as Function by A1; rng (the_arity_of o) = {} by A1,FINSEQ_1:27; then rng (the_arity_of o) c= dom F by XBOOLE_1:2; then A3: dom (F*the_arity_of o) = dom (the_arity_of o) by RELAT_1:46 .= {} by A1,FINSEQ_1:26; then rng (F*the_arity_of o) = {} by RELAT_1:65; then (F*the_arity_of o) is Function of {},{} by A3,FUNCT_2:3; then product (doms (F*the_arity_of o)) = {{}} by CARD_3:19,FUNCT_6:32,PARTFUN1:57; then A4: e1 in product (doms (F*the_arity_of o)) by A1,TARSKI:def 1; A5: F#e = (Frege(F*the_arity_of o)).e by A2,MSUALG_3:def 7 .= (F*the_arity_of o)..e1 by A4,PRALG_2:def 8; then reconsider fn = F#e as Function; A6: dom fn = {} by A3,A5,PRALG_1:def 18; then reconsider fin = F#e as FinSequence by FINSEQ_1:4,def 2; fin = {} by A6,FINSEQ_1:26; hence thesis; end; begin :: Properties of Arguments of operations in Many Sorted Algebras theorem Th13: for U1,U2 be non-empty MSAlgebra over S for F be ManySortedFunction of U1,U2 for x be Element of Args(o,U1) holds x in product doms (F*the_arity_of o) proof let U1,U2 be non-empty MSAlgebra over S; let F be ManySortedFunction of U1,U2; let x be Element of Args(o,U1); dom F = (the carrier of S) by PBOOLE:def 3; then A1: rng (the_arity_of o) c= dom F; x in Args(o,U1); then A2:x in product ((the Sorts of U1)*(the_arity_of o)) by PRALG_2:10; then A3: dom x = dom ((the Sorts of U1)*(the_arity_of o)) by CARD_3:18 .= dom (the_arity_of o) by PRALG_2:10; A4: dom x = dom ((the Sorts of U1)*(the_arity_of o)) by A2,CARD_3:18; now let n be set; assume n in dom x; then A5: n in dom (F*the_arity_of o) by A1,A3,RELAT_1:46; (F*the_arity_of o).n is Function; then n in (F*the_arity_of o)"SubFuncs rng (F*the_arity_of o) by A5,FUNCT_6:28; hence n in dom (doms (F*the_arity_of o)) by FUNCT_6:def 2; end; then A6: dom x c= dom (doms (F*the_arity_of o)) by TARSKI:def 3; A7:now let n be set; assume n in dom (doms (F*the_arity_of o)); then n in (F*the_arity_of o)"SubFuncs rng (F*the_arity_of o) by FUNCT_6:def 2; then n in dom (F*the_arity_of o) by FUNCT_6:28; hence n in dom x by A1,A3,RELAT_1:46; end; then dom (doms (F*the_arity_of o)) c= dom x by TARSKI:def 3; then A8: dom x = dom (doms (F*the_arity_of o)) by A6,XBOOLE_0:def 10; now let n be set; assume A9: n in dom (doms (F*the_arity_of o)); then A10: n in dom (the_arity_of o) by A3,A7; then A11: n in dom (F*the_arity_of o) by A1,RELAT_1:46; A12: n in dom ((the Sorts of U1)*(the_arity_of o)) by A4,A7,A9; (the_arity_of o).n in rng (the_arity_of o) by A10,FUNCT_1:def 5; then reconsider s1 = (the_arity_of o).n as Element of (the carrier of S); (F*the_arity_of o).n = F.s1 by A11,FUNCT_1:22; then A13:(doms (F*the_arity_of o)).n = dom (F.s1) by A11,FUNCT_6:31 .= (the Sorts of U1).s1 by FUNCT_2:def 1; x.n in ((the Sorts of U1)*(the_arity_of o)).n by A2,A12,CARD_3:18; hence x.n in (doms (F*the_arity_of o)).n by A12,A13,FUNCT_1:22; end; hence x in product doms (F*the_arity_of o) by A8,CARD_3:18; end; theorem Th14: for U1,U2 be non-empty MSAlgebra over S for F be ManySortedFunction of U1,U2 for x be Element of Args(o,U1) for n be set st n in dom (the_arity_of o) holds (F#x).n = F.((the_arity_of o)/.n).(x.n) proof let U1,U2 be non-empty MSAlgebra over S; let F be ManySortedFunction of U1,U2; let x be Element of Args(o,U1); let n be set such that A1: n in dom (the_arity_of o); A2: x in product doms (F*the_arity_of o) by Th13; dom F = (the carrier of S) by PBOOLE:def 3; then rng (the_arity_of o) c= dom F; then A3: n in dom (F*the_arity_of o) by A1,RELAT_1:46; thus (F#x).n = ((Frege(F*the_arity_of o)).x).n by MSUALG_3:def 7 .= ((F*the_arity_of o)..x).n by A2,PRALG_2:def 8 .= ((F*the_arity_of o).n).(x.n) by A3,PRALG_1:def 18 .= (F.((the_arity_of o).n)).(x.n) by A3,FUNCT_1:22 .= F.((the_arity_of o)/.n).(x.n) by A1,FINSEQ_4:def 4; end; theorem Th15: for x be Element of Args(o,product A) holds x in Funcs (dom (the_arity_of o),Funcs (I,union { (the Sorts of A.i').s' where i' is Element of I,s' is Element of (the carrier of S) : not contradiction })) proof let x be Element of Args(o,product A); set C = union { (the Sorts of A.i').s' where i' is Element of I, s' is Element of (the carrier of S) : not contradiction }; dom (SORTS A) = the carrier of S by PBOOLE:def 3; then A1: rng (the_arity_of o) c= dom (SORTS A); x in Args(o,product A); then x in product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:10; then A2: x in product ((SORTS A)*(the_arity_of o)) by PRALG_2:20; then A3: dom x = dom ((SORTS A)*(the_arity_of o)) by CARD_3:18 .= dom (the_arity_of o) by A1,RELAT_1:46; consider x1 be Function such that A4: x1 = x; now let c be set; assume c in rng x1; then consider n be set such that A5: n in dom x1 & x1.n = c by FUNCT_1:def 5; A6: n in dom ((SORTS A)*(the_arity_of o)) by A2,A4,A5,CARD_3:18; then n in dom (the_arity_of o) by A1,RELAT_1:46; then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 5; then reconsider s1 = (the_arity_of o).n as Element of (the carrier of S); x1.n in ((SORTS A)*(the_arity_of o)).n by A2,A4,A6,CARD_3:18; then x1.n in (SORTS A).s1 by A6,FUNCT_1:22; then x1.n in product Carrier(A,s1) by PRALG_2:def 17; then consider g be Function such that A7: g = x1.n & dom g = dom Carrier(A,s1) & for i' be set st i' in dom (Carrier(A,s1)) holds g.i' in (Carrier(A,s1)).i' by CARD_3:def 5; A8: dom g = I by A7,PBOOLE:def 3; now let c1 be set; assume c1 in rng g; then consider i1 be set such that A9: i1 in dom g & g.i1 = c1 by FUNCT_1:def 5; reconsider i1 as Element of I by A7,A9,PBOOLE:def 3; consider U0 being MSAlgebra over S such that A10:U0 = A.i1 & (Carrier(A,s1)).i1 = (the Sorts of U0).s1 by PRALG_2:def 16; A11:g.i1 in (the Sorts of A.i1).s1 by A7,A9,A10; (the Sorts of A.i1).s1 in {(the Sorts of A.i').s' where i' is Element of I, s' is Element of (the carrier of S) : not contradiction }; hence c1 in C by A9,A11,TARSKI:def 4; end; then rng g c= C by TARSKI:def 3; hence c in Funcs(I,C) by A5,A7,A8,FUNCT_2:def 2; end; then rng x1 c= Funcs(I,C) by TARSKI:def 3; hence x in Funcs(dom (the_arity_of o),Funcs(I,C)) by A3,A4,FUNCT_2:def 2; end; theorem Th16: for x be Element of Args(o,product A) for n be set st n in dom (the_arity_of o) holds x.n in product Carrier(A,(the_arity_of o)/.n) proof let x be Element of Args(o,product A); let n be set such that A1:n in dom (the_arity_of o); x in Args(o,product A); then x in product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:10; then A2: x in product ((SORTS A)*(the_arity_of o)) by PRALG_2:20; dom (SORTS A) = the carrier of S by PBOOLE:def 3; then rng (the_arity_of o) c= dom (SORTS A); then A3:n in dom ((SORTS A)*(the_arity_of o)) by A1,RELAT_1:46; then x.n in ((SORTS A)*(the_arity_of o)).n by A2,CARD_3:18; then x.n in (SORTS A).((the_arity_of o).n) by A3,FUNCT_1:22; then x.n in (SORTS A).((the_arity_of o)/.n) by A1,FINSEQ_4:def 4; hence thesis by PRALG_2:def 17; end; theorem Th17: for i be Element of I for n be set st n in dom(the_arity_of o) for s be SortSymbol of S st s = (the_arity_of o).n for y be Element of Args(o,product A) for g be Function st g = y.n holds g.i in (the Sorts of A.i).s proof let i be Element of I; let n be set such that A1: n in dom(the_arity_of o); let s be SortSymbol of S such that A2: s = (the_arity_of o).n; let y be Element of Args(o,product A); let g be Function such that A3: g = y.n; A4: n in dom ((the Sorts of (product A))*(the_arity_of o)) by A1,PRALG_2:10; i in I; then A5: i in dom (Carrier(A,s)) by PBOOLE:def 3; y in Args(o,product A); then y in product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:10; then g in ((the Sorts of (product A))*(the_arity_of o)).n by A3,A4,CARD_3:18; then g in (the Sorts of (product A)).s by A2,A4,FUNCT_1:22; then g in (SORTS A).s by PRALG_2:20; then A6:g in product Carrier(A,s) by PRALG_2:def 17; consider U0 being MSAlgebra over S such that A7:U0 = A.i & (Carrier(A,s)).i = (the Sorts of U0).s by PRALG_2:def 16; thus g.i in (the Sorts of A.i).s by A5,A6,A7,CARD_3:18; end; theorem Th18: for y be Element of Args(o,product A) st (the_arity_of o) <> {} holds (commute y) in product doms (A?.o) proof let y be Element of Args(o,product A); assume (the_arity_of o) <> {}; then A1: dom (the_arity_of o) <> {} by FINSEQ_1:26; set D = union { (the Sorts of A.i').s' where i' is Element of I,s' is Element of (the carrier of S) : not contradiction }; A2:y in Funcs (dom (the_arity_of o),Funcs (I,D)) by Th15; then commute y in Funcs (I,Funcs (dom (the_arity_of o),D)) by A1,PRALG_2:4; then consider f be Function such that A3: f = commute y & dom f = I & rng f c= Funcs (dom (the_arity_of o),D) by FUNCT_2:def 2; A4: dom (commute y) = dom (doms (A?.o)) by A3,PRALG_2:18; now let i1 be set; assume i1 in dom (doms (A?.o)); then reconsider ii =i1 as Element of I by PRALG_2:18; (commute y).ii in rng (commute y) by A3,FUNCT_1:def 5; then consider h be Function such that A5: h = (commute y).ii & dom h = dom (the_arity_of o) & rng h c= D by A3,FUNCT_2:def 2; A6: dom((commute y).ii) = dom ((the Sorts of A.ii)*(the_arity_of o)) by A5, PRALG_2:10; now let n be set; assume A7: n in dom ((the Sorts of A.ii)*(the_arity_of o)); then A8: n in dom (the_arity_of o) by PRALG_2:10; then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 5; then reconsider s1 = (the_arity_of o).n as SortSymbol of S; consider ff be Function such that A9: ff = y & dom ff = dom (the_arity_of o) & rng ff c= Funcs(I,D) by A2,FUNCT_2:def 2; n in dom y by A7,A9,PRALG_2:10; then y.n in rng y by FUNCT_1:def 5; then consider g be Function such that A10: g = y.n & dom g = I & rng g c= D by A9,FUNCT_2:def 2; A11: ((commute y).ii).n = g.ii by A2,A8,A10,PRALG_2:5; g.ii in (the Sorts of A.ii).s1 by A8,A10,Th17; hence ((commute y).ii).n in ((the Sorts of A.ii)*(the_arity_of o)).n by A7,A11,FUNCT_1:22; end; then (commute y).ii in product ((the Sorts of A.ii)*(the_arity_of o)) by A6,CARD_3:18; then (commute y).ii in Args(o,A.ii) by PRALG_2:10; hence (commute y).i1 in (doms (A?.o)).i1 by PRALG_2:18; end; hence (commute y) in product doms (A?.o) by A4,CARD_3:18; end; theorem Th19: for y be Element of Args(o,product A) st the_arity_of o <> {} holds y in dom (Commute Frege(A?.o)) proof let y be Element of Args(o,product A); assume A1:the_arity_of o <> {}; then (commute y) in product doms (A?.o) by Th18; then A2: (commute y) in dom (Frege(A?.o)) by PBOOLE:def 3; set D = union { (the Sorts of A.ii).ss where ii is Element of I,ss is Element of (the carrier of S) : not contradiction }; A3:y in Funcs (dom (the_arity_of o),Funcs (I,D)) by Th15; dom(the_arity_of o) <> {} by A1,FINSEQ_1:26; then y = commute commute y by A3,PRALG_2:6; hence y in dom (Commute Frege(A?.o)) by A2,PRALG_2:def 6; end; theorem Th20: for I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I,S, o be OperSymbol of S for x be Element of Args(o,product A) holds Den(o,product A).x in product Carrier(A,the_result_sort_of o) proof let I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I,S, o be OperSymbol of S; let x be Element of Args(o,product A); Result(o,product A) = (the Sorts of product A).(the_result_sort_of o) by PRALG_2:10 .= (SORTS A).(the_result_sort_of o) by PRALG_2:20 .= product Carrier(A,the_result_sort_of o) by PRALG_2:def 17; hence Den(o,product A).x in product Carrier(A,the_result_sort_of o); end; theorem Th21: for I,S,A,i for o be OperSymbol of S st (the_arity_of o) <> {} for U1 be non-empty MSAlgebra over S for x be Element of Args(o,product A) holds (commute x).i is Element of Args(o,A.i) proof let I,S,A,i; let o be OperSymbol of S such that A1: (the_arity_of o) <> {}; let U1 be non-empty MSAlgebra over S; let x be Element of Args(o,product A); i in I; then A2: i in dom (doms(A?.o)) by PRALG_2:18; (commute x) in product doms(A?.o) by A1,Th18; then (commute x).i in doms(A?.o).i by A2,CARD_3:18; hence (commute x).i is Element of Args(o,A.i) by PRALG_2:18; end; theorem Th22: for I,S,A,i,o for x be Element of Args(o,product A) for n be set st n in dom(the_arity_of o) for f be Function st f = x.n holds ((commute x).i).n = f.i proof let I,S,A,i,o; let x be Element of Args(o,product A); let n be set such that A1: n in dom(the_arity_of o); let g be Function such that A2: g = x.n; set C = union { (the Sorts of A.i').s' where i' is Element of I,s' is Element of (the carrier of S) : not contradiction }; x in Funcs (dom (the_arity_of o),Funcs (I,C)) by Th15; hence ((commute x).i).n = g.i by A1,A2,PRALG_2:5; end; theorem Th23: for o be OperSymbol of S st (the_arity_of o) <> {} for y be Element of Args(o,product A), i' be Element of I for g be Function st g = Den(o,product A).y holds g.i' = Den(o,A.i').((commute y).i') proof let o be OperSymbol of S such that A1: (the_arity_of o) <> {}; let y be Element of Args(o,product A), i' be Element of I; let g be Function such that A2: g = Den(o,product A).y; A3: Den(o,product A) = (the Charact of (product A)).o by MSUALG_1:def 11 .= (OPS A).o by PRALG_2:20 .= IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)) by PRALG_2:def 20 .= (Commute Frege(A?.o)) by A1,CQC_LANG:def 1; A4: y in dom (Commute Frege(A?.o)) by A1,Th19; A5: (commute y) in product doms (A?.o) by A1,Th18; A6: dom (A?.o) = I by PBOOLE:def 3; g = (Frege(A?.o)).(commute y) by A2,A3,A4,PRALG_2:def 6 .= (A?.o)..(commute y) by A5,PRALG_2:def 8; then g.i' = ((A?.o).i').((commute y).i') by A6,PRALG_1:def 18 .= Den(o,A.i').((commute y).i') by PRALG_2:14; hence thesis; end; begin :: The Projection of Family of Many Sorted Algebras definition let f be Function, x be set; func proj(f,x) -> Function means :Def2: dom it = product f & for y being Function st y in dom it holds it.y = y.x; existence proof defpred P[set,set] means for x' be Function st $1 = x' holds $2 = x'.x; A1: now let q,y1,y2 be set such that A2: q in product f and A3: P[q,y1] and A4: P[q,y2]; reconsider x1 = q as Function by A2,Lm1; thus y1 = x1.x by A3 .= y2 by A4; end; A5:now let q be set; assume q in product f; then reconsider q1 = q as Function by Lm1; take y = q1.x; thus P[q,y]; end; consider F be Function such that A6: dom F = product f & for a being set st a in product f holds P[a,F.a] from FuncEx(A1,A5); take F; thus thesis by A6; end; uniqueness proof let F,G be Function such that A7: dom F = product f & for y being Function st y in dom F holds F.y = y.x and A8: dom G = product f & for y being Function st y in dom G holds G.y = y.x; now let x' be set; assume A9: x' in product f; then reconsider x1 = x' as Function by Lm1; thus F.x' = x1.x by A7,A9 .= G.x' by A8,A9; end; hence thesis by A7,A8,FUNCT_1:9; end; end; definition let I,S; let A be MSAlgebra-Family of I,S, i be Element of I; func proj(A,i) -> ManySortedFunction of product A,A.i means :Def3: for s be Element of S holds it.s = proj (Carrier(A,s), i); existence proof deffunc G(Element of S) = proj (Carrier(A,$1), i); consider F be ManySortedSet of the carrier of S such that A1: for s be Element of S holds F.s = G(s) from LambdaDMS; F is ManySortedFunction of product A,A.i proof let s be set such that A2: s in the carrier of S; F.s is Function of (the Sorts of product A).s , (the Sorts of A.i).s proof reconsider s' = s as Element of S by A2; F.s = proj (Carrier(A,s'),i) by A1; then reconsider F' = F.s as Function; A3: (the Sorts of A.i).s is non empty by A2,PBOOLE:def 16; A4: dom F' = dom (proj (Carrier(A,s'),i)) by A1 .= product (Carrier(A,s')) by Def2 .= (SORTS A).s by PRALG_2:def 17 .= (the Sorts of product A).s by PRALG_2:20; rng F' c= (the Sorts of A.i).s proof let y be set; assume y in rng F'; then y in rng (proj (Carrier(A,s'),i)) by A1; then consider x1 be set such that A5: x1 in dom (proj (Carrier(A,s'),i)) and A6: y = (proj (Carrier(A,s'),i)).x1 by FUNCT_1:def 5; A7: x1 in product (Carrier(A,s')) by A5,Def2; then reconsider x1 as Function by Lm1; A8: dom (Carrier(A,s')) = I by PBOOLE:def 3; A9: y = x1.i by A5,A6,Def2; consider U0 being MSAlgebra over S such that A10:U0 = A.i & (Carrier(A,s')).i = (the Sorts of U0).s' by PRALG_2:def 16; thus y in (the Sorts of A.i).s by A7,A8,A9,A10,CARD_3:18; end; hence thesis by A3,A4,FUNCT_2:def 1,RELSET_1:11; end; hence thesis; end; then reconsider F' = F as ManySortedFunction of product A,A.i; take F'; thus thesis by A1; end; uniqueness proof let F,G be ManySortedFunction of product A,A.i such that A11: for s be Element of S holds F.s = proj (Carrier(A,s), i) and A12: for s be Element of S holds G.s = proj (Carrier(A,s), i); now let s' be set; assume s' in (the carrier of S); then reconsider s'' = s' as Element of S; thus F.s' = proj (Carrier(A,s''), i) by A11 .= G.s' by A12; end; hence F = G by PBOOLE:3; end; end; theorem Th24: for x be Element of Args(o,product A) st Args(o,product A) <> {} & the_arity_of o <> {} for i be Element of I holds proj(A,i)#x = (commute x).i proof let x be Element of Args(o,product A) such that A1: Args(o,product A) <> {} & the_arity_of o <> {}; let i be Element of I; set C = union { (the Sorts of A.i').s' where i' is Element of I, s' is Element of (the carrier of S) : not contradiction }; dom (proj(A,i)) = (the carrier of S) by PBOOLE:def 3; then A2: rng (the_arity_of o) c= dom (proj(A,i)); A3:dom (the_arity_of o) <> {} by A1,FINSEQ_1:26; A4:x in Funcs (dom (the_arity_of o),Funcs(I,C)) by Th15; then commute x in Funcs(I,Funcs(dom (the_arity_of o),C)) by A3,PRALG_2:4; then A5:dom (commute x) = I & rng (commute x) c= Funcs(dom (the_arity_of o),C) by Th4; then (commute x).i in rng (commute x) by FUNCT_1:def 5; then A6: dom ((commute x).i) = dom (the_arity_of o) by A5,Th4; A7: x in product doms ((proj(A,i))*the_arity_of o) by Th13; A8:dom ((proj(A,i))#x) = dom ((Frege((proj(A,i))*the_arity_of o)).x) by MSUALG_3:def 7 .= dom (((proj(A,i))*the_arity_of o)..x) by A7,PRALG_2:def 8 .= dom ((proj(A,i))*the_arity_of o) by PRALG_1:def 18 .= dom (the_arity_of o) by A2,RELAT_1:46; now let n be set such that A9:n in dom (the_arity_of o); A10:dom x = dom (the_arity_of o) & rng x c= Funcs(I,C) by A4,Th4; n in dom x by A4,A9,Th4; then x.n in rng x by FUNCT_1:def 5; then consider g be Function such that A11: g = x.n & dom g = I & rng g c= C by A10,FUNCT_2:def 2; x.n in product Carrier(A,(the_arity_of o)/.n) by A9,Th16; then A12: x.n in dom (proj (Carrier(A,(the_arity_of o)/.n),i)) by Def2; thus ((proj(A,i))#x).n = ((proj(A,i)).((the_arity_of o)/.n)).(x.n) by A9,Th14 .= (proj (Carrier(A,(the_arity_of o)/.n),i)).(x.n) by Def3 .= g.i by A11,A12,Def2 .= ((commute x).i).n by A4,A9,A11,PRALG_2:5; end; hence (proj(A,i))#x = (commute x).i by A6,A8,FUNCT_1:9; end; theorem for i be Element of I for A be MSAlgebra-Family of I,S holds proj(A,i) is_homomorphism product A,A.i proof let i be Element of I; let A be MSAlgebra-Family of I,S; thus proj(A,i) is_homomorphism product A,A.i proof let o be OperSymbol of S such that Args(o,product A) <> {}; let x be Element of Args(o,product A); set F = proj(A,i), s = the_result_sort_of o; o in the OperSymbols of S; then A1: o in dom (the ResultSort of S) by FUNCT_2:def 1; A2:Result(o,product A) = ((the Sorts of product A) * the ResultSort of S).o by MSUALG_1:def 10 .= (the Sorts of product A).((the ResultSort of S).o) by A1,FUNCT_1:23 .= (the Sorts of product A).(the_result_sort_of o) by MSUALG_1:def 7 .= (SORTS A).s by PRALG_2:20 .= product Carrier(A,s) by PRALG_2:def 17; thus (F.s).(Den(o,product A).x) = Den(o,A.i).(F#x) proof per cases; suppose A3: the_arity_of o = {}; then A4: Args(o,product A) = {{}} by PRALG_2:11; then A5: x = {} by TARSKI:def 1; const(o,product A) in product(Carrier(A,s)) by A2,A3,Th6; then A6: const(o,product A) in dom (proj (Carrier(A,s),i)) by Def2; (F.s).(Den(o,product A).x) = (F.s).(Den(o,product A).{}) by A4,TARSKI:def 1 .= (F.s).(const(o,product A)) by Def1 .= (proj (Carrier(A,s),i)).(const(o,product A)) by Def3 .= (const(o,product A)).i by A6,Def2 .= const(o,A.i) by A3,Th10 .= Den(o,A.i).{} by Def1 .= Den(o,A.i).(F#x) by A3,A5,Th12; hence thesis; suppose A7: the_arity_of o <> {}; (Den(o,product A).x) in product Carrier(A,s) by A2; then A8: (Den(o,product A).x) in dom (proj (Carrier(A,s),i)) by Def2; reconsider D = (Den(o,product A).x) as Function by A2,Lm1; (F.s).(Den(o,product A).x) = (proj (Carrier(A,s),i)).(Den(o,product A).x) by Def3 .= D.i by A8,Def2 .= (Den(o,A.i)).((commute x).i) by A7,Th23 .= (Den(o,A.i)).(proj(A,i)#x) by A7,Th24; hence thesis; end; end; end; theorem Th26: for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds F in Funcs(I,Funcs(the carrier of S, {F.i'.s1 where s1 is SortSymbol of S,i' is Element of I :not contradiction})) & (commute F).s.i = F.i.s proof let U1 be non-empty MSAlgebra over S; let F be ManySortedFunction of I such that A1:(for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i); set FS = {F.i'.s1 where s1 is SortSymbol of S,i' is Element of I :not contradiction}, CA = the carrier of S; A2:dom F = I by PBOOLE:def 3; A3: rng F c= Funcs(CA,FS) proof let x be set; assume x in rng F; then consider i' be set such that A4: i' in dom F & F.i' = x by FUNCT_1:def 5; reconsider i1 = i' as Element of I by A4,PBOOLE:def 3; consider F' being ManySortedFunction of U1,A.i1 such that A5: F' = F.i1 & F' is_homomorphism U1,A.i1 by A1; A6: dom F' = CA by PBOOLE:def 3; rng F' c= FS proof let x' be set; assume x' in rng F'; then consider s' be set such that A7: s' in dom F' & F'.s' = x' by FUNCT_1:def 5; s' is SortSymbol of S by A7,PBOOLE:def 3; hence x' in FS by A5,A7; end; hence x in Funcs(CA,FS) by A4,A5,A6,FUNCT_2:def 2; end; then A8:F in Funcs(I,Funcs(CA,FS)) by A2,FUNCT_2:def 2; thus F in Funcs(I,Funcs(CA,FS)) by A2,A3,FUNCT_2:def 2; thus (commute F).s.i = F.i.s by A8,PRALG_2:5; end; theorem Th27: for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds (commute F).s in Funcs(I,Funcs((the Sorts of U1).s, union {(the Sorts of A.i').s1 where i' is Element of I,s1 is SortSymbol of S : not contradiction})) proof let U1 be non-empty MSAlgebra over S; let F be ManySortedFunction of I such that A1: (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i); set SU = the Sorts of U1, CA = the carrier of S, SA = union {(the Sorts of A.i').s1 where i' is Element of I,s1 is SortSymbol of S : not contradiction}, SA' = {(the Sorts of A.i').s1 where i' is Element of I,s1 is SortSymbol of S : not contradiction}, FS = {F.i'.s1 where s1 is SortSymbol of S,i' is Element of I :not contradiction}; F in Funcs(I,Funcs(CA,FS)) by A1,Th26; then commute F in Funcs(CA,Funcs(I,FS)) by PRALG_2:4; then consider F' be Function such that A2: F' = commute F & dom F' = CA & rng F' c= Funcs(I,FS) by FUNCT_2:def 2; (commute F).s in rng F' by A2,FUNCT_1:def 5; then consider F2 be Function such that A3:F2 = (commute F).s & dom F2 = I & rng F2 c= FS by A2,FUNCT_2:def 2; rng ((commute F).s) c= Funcs(SU.s,SA) proof let x' be set; assume x' in rng ((commute F).s); then consider i' be set such that A4:i' in dom ((commute F).s) & x' = ((commute F).s).i' by FUNCT_1:def 5; reconsider i1 = i' as Element of I by A3,A4; consider F' be ManySortedFunction of U1,A.i1 such that A5: F' = F.i1 & F' is_homomorphism U1,A.i1 by A1; A6:x' = F'.s by A1,A4,A5,Th26; A7:dom (F'.s) = SU.s by FUNCT_2:def 1; (the Sorts of A.i1).s c= SA proof let y be set such that A8:y in (the Sorts of A.i1).s; (the Sorts of A.i1).s in SA'; hence y in SA by A8,TARSKI:def 4; end; then rng (F'.s) c= SA by XBOOLE_1:1; hence x' in Funcs(SU.s,SA) by A6,A7,FUNCT_2:def 2; end; hence (commute F).s in Funcs(I,Funcs(SU.s,SA)) by A3,FUNCT_2:def 2; end; theorem Th28: for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) for F' be ManySortedFunction of U1,A.i st F' = F.i for x be set st x in (the Sorts of U1).s for f be Function st f = (commute((commute F).s)).x holds f.i = F'.s.x proof let U1 be non-empty MSAlgebra over S; let F be ManySortedFunction of I such that A1: (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i); let F' be ManySortedFunction of U1,A.i such that A2: F' = F.i; let x1 be set such that A3: x1 in (the Sorts of U1).s; let f be Function such that A4: f = (commute((commute F).s)).x1; set SU = the Sorts of U1, SA = union {(the Sorts of A.i').s1 where i' is Element of I,s1 is SortSymbol of S : not contradiction}; reconsider f' = (commute F).s as Function; A5:(commute F).s in Funcs (I,Funcs(SU.s,SA)) by A1,Th27; then A6:dom ((commute F).s) = I by Th4; A7:rng ((commute F).s) c= Funcs(SU.s,SA) by A5,Th4; ((commute F).s).i in rng ((commute F).s) by A6,FUNCT_1:def 5; then consider g be Function such that A8:g = f'.i & dom g = SU.s & rng g c= SA by A7,FUNCT_2:def 2; g = F'.s by A1,A2,A8,Th26; hence f.i = F'.s.x1 by A3,A4,A5,A8,PRALG_2:5; end; theorem Th29: for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) for x be set st x in (the Sorts of U1).s holds (commute ((commute F).s)).x in product (Carrier(A,s)) proof let U1 be non-empty MSAlgebra over S; let F be ManySortedFunction of I such that A1: (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i); let x be set such that A2: x in (the Sorts of U1).s; set SU = the Sorts of U1, SA = union {(the Sorts of A.i').s1 where i' is Element of I,s1 is SortSymbol of S : not contradiction}; (commute F).s in Funcs (I,Funcs(SU.s,SA)) by A1,Th27; then commute ((commute F).s) in Funcs (SU.s,Funcs(I,SA)) by PRALG_2:4; then consider f' be Function such that A3: f' = (commute (commute F).s) & dom f' = SU.s & rng f' c= Funcs(I,SA) by FUNCT_2:def 2; f'.x in rng f' by A2,A3,FUNCT_1:def 5; then consider f be Function such that A4: f = (commute (commute F).s).x & dom f = I & rng f c= SA by A3,FUNCT_2:def 2; A5:dom ((commute (commute F).s).x) = dom (Carrier(A,s)) by A4,PBOOLE:def 3; now let i1 be set; assume i1 in dom ((Carrier(A,s))); then reconsider i' = i1 as Element of I by PBOOLE:def 3; consider F1 be ManySortedFunction of U1,A.i' such that A6: F1 = F.i' & F1 is_homomorphism U1,A.i' by A1; A7: f.i' = F1.s.x by A1,A2,A4,A6,Th28; consider U0 being MSAlgebra over S such that A8:U0 = A.i' & (Carrier(A,s)).i' = (the Sorts of U0).s by PRALG_2:def 16; x in dom (F1.s) by A2,FUNCT_2:def 1; then F1.s.x in rng (F1.s) by FUNCT_1:def 5; hence ((commute ((commute F).s)).x).i1 in ((Carrier(A,s))).i1 by A4,A7,A8; end; hence (commute ((commute F).s)).x in product (Carrier(A,s)) by A5,CARD_3:18; end; theorem for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds ex H being ManySortedFunction of U1,(product A) st H is_homomorphism U1,(product A) & (for i be Element of I holds proj(A,i) ** H = F.i) proof let U1 be non-empty MSAlgebra over S; let F be ManySortedFunction of I such that A1: (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i); deffunc G(Element of S) = commute((commute F).$1); consider H being ManySortedSet of (the carrier of S) such that A2:for s' be Element of (the carrier of S) holds H.s' = G(s') from LambdaDMS; set SU = the Sorts of U1, CA = the carrier of S, SA = union {(the Sorts of A.i').s1 where i' is Element of I,s1 is SortSymbol of S : not contradiction}; now let s' be set; assume A3: s' in (the carrier of S); then s' in dom SU by PBOOLE:def 3; then A4: SU.s' <> {} by UNIALG_1:def 6; reconsider s'' = s' as SortSymbol of S by A3; (commute F).s' in Funcs (I,Funcs(SU.s',SA)) by A1,A3,Th27; then commute ((commute F).s') in Funcs (SU.s',Funcs(I,SA)) by A4,PRALG_2:4; then H.s' in Funcs(SU.s',Funcs(I,SA)) by A2,A3; then consider Hs be Function such that A5: Hs = H.s' & dom Hs = SU.s' & rng Hs c= Funcs(I,SA) by FUNCT_2:def 2; s' in dom (SORTS A) by A3,PBOOLE:def 3; then (SORTS A).s' is non empty by UNIALG_1:def 6; then A6: (the Sorts of (product A)).s' is non empty by PRALG_2:20; rng Hs c= (the Sorts of (product A)).s' proof let x be set; assume A7: x in rng Hs; then consider f be Function such that A8: f = x & dom f = I & rng f c= SA by A5,FUNCT_2:def 2; A9: dom Carrier(A,s'') = dom f by A8,PBOOLE:def 3; consider x1 be set such that A10: x1 in dom Hs & Hs.x1 = f by A7,A8,FUNCT_1:def 5; now let i' be set; assume i' in dom Carrier(A,s''); then reconsider i'' = i' as Element of I by PBOOLE:def 3; A11: H.s'' = commute ((commute F).s'') by A2; consider F' be ManySortedFunction of U1,A.i'' such that A12: F' = F.i'' & F' is_homomorphism U1,A.i'' by A1; A13: f.i'' = F'.s''.x1 by A1,A5,A10,A11,A12,Th28; consider U0 being MSAlgebra over S such that A14:U0 = A.i'' & (Carrier(A,s'')).i'' =(the Sorts of U0).s'' by PRALG_2:def 16; A15:rng (F'.s'') c= (the Sorts of A.i'').s''; dom (F'.s'') = dom Hs by A5,FUNCT_2:def 1; then F'.s'.x1 in rng (F'.s') by A10,FUNCT_1:def 5; hence f.i' in Carrier(A,s'').i' by A13,A14,A15; end; then f in product Carrier(A,s'') by A9,CARD_3:18; then f in (SORTS A).s'' by PRALG_2:def 17; hence x in (the Sorts of (product A)).s' by A8,PRALG_2:20; end; hence H.s' is Function of (the Sorts of U1).s', (the Sorts of (product A)).s' by A5,A6,FUNCT_2: def 1,RELSET_1:11; end; then reconsider H as ManySortedFunction of U1,(product A) by MSUALG_1:def 2; take H; A16: H is_homomorphism U1,(product A) proof let o be OperSymbol of S such that Args(o,U1) <> {}; let x be Element of Args(o,U1); set s' = the_result_sort_of o; A17: Result(o,U1) = (the Sorts of U1).(the_result_sort_of o) by PRALG_2:10; then A18:(Den(o,U1).x) in SU.s'; thus (H.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,(product A)).(H#x) proof per cases; suppose A19: the_arity_of o = {}; set f = (commute ((commute F).s')).const(o,U1); Args(o,U1) = {{}} by A19,PRALG_2:11; then A20: x = {} by TARSKI:def 1; then A21:H#x = {} by A19,Th12; A22:const(o,U1) in SU.s' by A18,A20,Def1; then f in product (Carrier(A,s')) by A1,Th29; then A23:dom f = dom (Carrier(A,s')) by CARD_3:18 .= I by PBOOLE:def 3; const(o,product A) in Funcs(I,union { Result(o,A.i1) where i1 is Element of I: not contradiction }) by A19,Th9; then consider Co be Function such that A24: Co = const(o,product A) & dom Co = I & rng Co c= union { Result(o,A.i1) where i1 is Element of I: not contradiction } by FUNCT_2:def 2; now let i' be set; assume i' in I; then reconsider ii = i' as Element of I; consider F1 be ManySortedFunction of U1,A.ii such that A25: F1 = F.ii & F1 is_homomorphism U1,A.ii by A1; A26:F1#x = {} by A19,A20,Th12; thus f.i' = F1.s'.const(o,U1) by A1,A22,A25,Th28 .= (F1.(the_result_sort_of o)).(Den(o,U1).x) by A20,Def1 .= Den(o,A.ii).{} by A25,A26,MSUALG_3:def 9 .= const(o,A.ii) by Def1 .= (const(o,product A)).i' by A19,Th10; end; then A27: f = const(o,product A) by A23,A24,FUNCT_1:9; (H.(the_result_sort_of o)).(Den(o,U1).x) = (H.s').const(o,U1) by A20,Def1 .= const(o,product A) by A2,A27 .= Den(o,(product A)).(H#x) by A21,Def1; hence thesis; suppose A28: the_arity_of o <> {}; set f = (commute ((commute F).s')).(Den(o,U1).x); A29:Den(o,product A) = (the Charact of (product A)).o by MSUALG_1:def 11 .= (OPS A).o by PRALG_2:20 .= IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)) by PRALG_2:def 20 .= Commute Frege(A?.o) by A28,CQC_LANG:def 1; A30:now let y be Element of Args(o,product A); y in dom (Commute Frege(A?.o)) by A28,Th19; then A31: Den(o,product A).y = (Frege(A?.o)).(commute y) by A29,PRALG_2:def 6; (commute y) in product doms (A?.o) by A28,Th18; then (commute y) in dom (Frege(A?.o)) by PBOOLE:def 3; hence Den(o,product A).y in rng (Frege(A?.o)) by A31,FUNCT_1:def 5; end; then Den(o,product A).(H#x) in rng (Frege(A?.o)); then reconsider f1 = Den(o,(product A)).(H#x) as Function by PRALG_2:15; set D = union { (the Sorts of A.i').ss where i' is Element of I,ss is Element of (the carrier of S) : not contradiction }; A32:(H#x) in Funcs (dom (the_arity_of o),Funcs (I,D)) by Th15; (commute ((commute F).s')).(Den(o,U1).x) in product(Carrier(A,s')) by A1,A17,Th29; then A33: dom f = dom (Carrier(A,s')) by CARD_3:18 .= I by PBOOLE:def 3; f1 in rng (Frege(A?.o)) by A30; then A34:dom f1 = I by PRALG_2:16; now let i' be set; assume i' in I; then reconsider ii = i' as Element of I; consider F1 be ManySortedFunction of U1,A.ii such that A35: F1 = F.ii & F1 is_homomorphism U1,A.ii by A1; A36:(F1.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,A.ii).(F1#x) by A35,MSUALG_3:def 9; dom F1 = (the carrier of S) by PBOOLE:def 3; then A37: rng (the_arity_of o) c= dom F1; A38:x in product doms (F1*the_arity_of o) by Th13; A39:dom (F1#x) = dom ((Frege(F1*the_arity_of o)).x) by MSUALG_3:def 7 .= dom ((F1*the_arity_of o)..x) by A38,PRALG_2:def 8 .= dom (F1*the_arity_of o) by PRALG_1:def 18 .= dom (the_arity_of o) by A37,RELAT_1:46; dom (the_arity_of o) <> {} by A28,FINSEQ_1:26; then commute (H#x) in Funcs (I,Funcs (dom(the_arity_of o),D)) by A32,PRALG_2:4 ; then consider ff be Function such that A40:ff = commute (H#x) & dom ff = I & rng ff c= Funcs (dom(the_arity_of o),D) by FUNCT_2:def 2; ff.ii in rng ff by A40,FUNCT_1:def 5; then consider gg be Function such that A41: gg = (commute (H#x)).ii & dom gg = dom(the_arity_of o) & rng gg c= D by A40,FUNCT_2:def 2; now let n be set; assume A42: n in dom (the_arity_of o); then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 5; then reconsider s1 = (the_arity_of o).n as Element of (the carrier of S); x in Args(o,U1); then A43: x in product ((the Sorts of U1)*(the_arity_of o)) by PRALG_2:10; then A44: dom x = dom ((the Sorts of U1)*(the_arity_of o)) by CARD_3:18 .= dom (the_arity_of o) by PRALG_2:10; A45: dom x = dom ((the Sorts of U1)*(the_arity_of o)) by A43,CARD_3:18; then x.n in ((the Sorts of U1)*(the_arity_of o)).n by A42,A43,A44,CARD_3:18; then A46:(x.n) in SU.s1 by A42,A44,A45,FUNCT_1:22; A47: (F1#x).n = F1.((the_arity_of o)/.n).(x.n) by A42,Th14 .= F1.s1.(x.n) by A42,FINSEQ_4:def 4; A48: (H#x).n = H.((the_arity_of o)/.n).(x.n) by A42,Th14 .= H.s1.(x.n) by A42,FINSEQ_4:def 4 .= (commute ((commute F).s1)).(x.n) by A2; then reconsider g = (H#x).n as Function; thus ((commute (H#x)).ii).n = g.ii by A32,A42,PRALG_2:5 .= (F1#x).n by A1,A35,A46,A47,A48,Th28; end; then F1#x = (commute (H#x)).ii by A39,A41,FUNCT_1:9; then f.i' = Den(o,A.ii).((commute (H#x)).ii) by A1,A17,A35,A36,Th28 .= f1.i' by A28,Th23; hence f.i' = f1.i'; end; then (commute ((commute F).s')).(Den(o,U1).x) = f1 by A33,A34,FUNCT_1:9; hence thesis by A2; end; end; for i be Element of I holds proj(A,i) ** H = F.i proof let i be Element of I; consider F1 be ManySortedFunction of U1,A.i such that A49: F1 = F.i & F1 is_homomorphism U1,A.i by A1; A50: dom(proj(A,i) ** H) = (dom proj(A,i)) /\ (dom H) by MSUALG_3:def 4 .= CA /\ (dom H) by PBOOLE:def 3 .= CA /\ CA by PBOOLE:def 3 .= CA; A51: dom F1 = CA by PBOOLE:def 3; now let s' be set; assume s' in CA; then reconsider s1 = s' as SortSymbol of S; (commute F).s1 in Funcs (I,Funcs(SU.s1,SA)) by A1,Th27; then commute ((commute F).s1) in Funcs (SU.s1,Funcs(I,SA)) by PRALG_2:4; then consider f' be Function such that A52: f' = (commute (commute F).s1) & dom f' = SU.s1 & rng f' c= Funcs(I,SA) by FUNCT_2:def 2; A53:rng f' c= dom (proj (Carrier(A,s1),i)) proof let y be set; assume y in rng f'; then consider x' be set such that A54: x' in dom f' & f'.x' = y by FUNCT_1:def 5; (commute (commute F).s1).x' in product (Carrier(A,s1)) by A1,A52,A54, Th29 ; hence y in dom (proj (Carrier(A,s1),i)) by A52,A54,Def2; end; A55: (proj(A,i) ** H).s' = (proj(A,i).s1)*(H.s1) by A50,MSUALG_3:def 4 .= (proj (Carrier(A,s1),i)) * (H.s1) by Def3 .= ((proj (Carrier(A,s1),i))) * (commute (commute F).s1) by A2; then A56:dom ((proj(A,i) ** H).s') = SU.s' by A52,A53,RELAT_1:46; A57: dom (F1.s') = dom (F1.s1) .= SU.s' by FUNCT_2:def 1; now let x be set; assume A58: x in SU.s'; then ((commute (commute F).s1).x) in product (Carrier(A,s1)) by A1,Th29; then A59: ((commute (commute F).s1).x) in dom (proj (Carrier(A,s1),i)) by Def2; thus ((proj(A,i) ** H).s').x = (proj (Carrier(A,s1),i)).((commute (commute F).s1).x) by A55,A56,A58,FUNCT_1:22 .= ((commute (commute F).s1).x).i by A59,Def2 .= F1.s'.x by A1,A49,A58,Th28; end; hence (proj(A,i) ** H).s' = F1.s' by A56,A57,FUNCT_1:9; end; hence proj(A,i) ** H = F.i by A49,A50,A51,FUNCT_1:9; end; hence thesis by A16; end; begin :: The Class of Family of Many Sorted Algebras definition let I,J,S; mode MSAlgebra-Class of S,J -> ManySortedSet of I means :Def4: for i be set st i in I holds it.i is MSAlgebra-Family of J.i,S; existence proof defpred P[set,set] means $2 is MSAlgebra-Family of J.$1,S; A1: for i be set st i in I ex F be set st P[i,F] proof let i be set such that i in I; consider F be MSAlgebra-Family of J.i,S; take F; thus thesis; end; consider C be ManySortedSet of I such that A2: for i be set st i in I holds P[i,C.i] from MSSEx(A1); take C; thus thesis by A2; end; end; definition let I,S,A,EqR; func A / EqR -> MSAlgebra-Class of S,id (Class EqR) means :Def5: for c st c in Class EqR holds it.c = A|c; existence proof thus ex X be MSAlgebra-Class of S,id Class EqR st for c st c in Class EqR holds X.c = A|c proof deffunc F(set) = A|$1; consider X be ManySortedSet of Class EqR such that A1: for c st c in Class EqR holds X.c = F(c) from MSSLambda; X is MSAlgebra-Class of S,id Class EqR proof let c be set; assume A2: c in Class EqR; A3: now thus dom (A|c) = (dom A) /\ c by RELAT_1:90 .= I /\ c by PBOOLE:def 3 .= c by A2,XBOOLE_1:28 .= (id Class EqR).c by A2,FUNCT_1:35; end; then reconsider ac = A|c as ManySortedSet of (id Class EqR).c by PBOOLE:def 3; ac is MSAlgebra-Family of (id Class EqR).c,S proof let i be set; assume A4: i in (id Class EqR).c; dom ac = c by A2,A3,FUNCT_1:35; then reconsider i' = i as Element of I by A2,A3,A4; A.i' is non-empty MSAlgebra over S; hence thesis by A3,A4,FUNCT_1:68; end; hence X.c is MSAlgebra-Family of (id Class EqR).c,S by A1,A2; end; then reconsider X as MSAlgebra-Class of S,id Class EqR; take X; thus thesis by A1; end; end; uniqueness proof for X, Y be MSAlgebra-Class of S,id Class EqR st (for c st c in Class EqR holds X.c = A|c) & for c st c in Class EqR holds Y.c = A|c holds X = Y proof let X, Y be MSAlgebra-Class of S,id Class EqR such that A5: (for c st c in Class EqR holds X.c = A|c) and A6: for c st c in Class EqR holds Y.c = A|c; now let c; assume A7: c in Class EqR; hence X.c = A|c by A5 .= Y.c by A6,A7; end; hence X = Y by PBOOLE:3; end; hence thesis; end; end; definition let I,S; let J be non-empty ManySortedSet of I; let C be MSAlgebra-Class of S,J; func product C -> MSAlgebra-Family of I,S means :Def6: for i st i in I ex Ji be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & it.i = product Cs; existence proof thus ex PC be MSAlgebra-Family of I,S st for i st i in I ex Ji be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & PC.i = product Cs proof defpred P[set,set] means ex Ji be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.$1 & Cs = C.$1 & $2 = product Cs; A1: now let i be set; assume A2: i in I; then reconsider Ji = J.i as non empty set by PBOOLE:def 16; reconsider Cs = C.i as MSAlgebra-Family of Ji,S by A2,Def4; consider a be set such that A3: a = product Cs; consider j be set such that A4: ex Ji be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & j = product Cs by A3; take j; thus P[i,j] by A4; end; consider PC be ManySortedSet of I such that A5: for i be set st i in I holds P[i,PC.i] from MSSEx(A1); now let i be set; assume i in I; then consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such that A6: Ji = J.i & Cs = C.i & PC.i = product Cs by A5; thus PC.i is non-empty MSAlgebra over S by A6; end; then reconsider PC as MSAlgebra-Family of I,S by PRALG_2:def 12; take PC; thus thesis by A5; end; end; uniqueness proof for PC1,PC2 be MSAlgebra-Family of I,S st (for i st i in I ex Ji be non empty set , Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & PC1.i = product Cs ) & for i st i in I ex Ji be non empty set , Cs be MSAlgebra-Family of Ji,S st Ji =J.i & Cs = C.i & PC2.i = product Cs holds PC1 = PC2 proof let PC1,PC2 be MSAlgebra-Family of I,S such that A7: (for i st i in I ex Ji be non empty set , Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & PC1.i = product Cs ) and A8: (for i st i in I ex Ji be non empty set , Cs be MSAlgebra-Family of Ji,S st Ji =J.i & Cs = C.i & PC2.i = product Cs); now let i1 be set; assume i1 in I; then reconsider i' = i1 as Element of I; consider Ji1 be non empty set, Cs1 be MSAlgebra-Family of Ji1,S such that A9: Ji1 = J.i' and A10: Cs1 = C.i' and A11: PC1.i' = product Cs1 by A7; consider Ji2 be non empty set, Cs2 be MSAlgebra-Family of Ji2,S such that A12: Ji2 = J.i' and A13: Cs2 = C.i' and A14: PC2.i' = product Cs2 by A8; thus PC1.i1 = PC2.i1 by A9,A10,A11,A12,A13,A14; end; hence PC1 = PC2 by PBOOLE:3; end; hence thesis; end; end; theorem for A be MSAlgebra-Family of I,S, EqR be Equivalence_Relation of I holds product A, product (product (A/EqR)) are_isomorphic proof let A be MSAlgebra-Family of I,S, EqR be Equivalence_Relation of I; set U1 = product A, U2 = product product (A/EqR); set U1' = the Sorts of U1, U2' = the Sorts of U2; defpred P[set,set,set] means for f1,g1 being Function st f1 = $2 & g1 = $1 for e being Element of Class EqR holds g1.e = f1|e; A1: for s be set st s in the carrier of S holds for x be set st x in U1'.s ex y be set st y in U2'.s & P[y,x,s] proof let s be set such that A2: s in the carrier of S; let x be set such that A3: x in U1'.s; reconsider s' = s as SortSymbol of S by A2; U1' = SORTS A by PRALG_2:20; then A4: U1'.s' = product Carrier(A,s') by PRALG_2:def 17; then reconsider x as Function by A3,Lm1; deffunc F(set) = x|$1; consider y being ManySortedSet of Class EqR such that A5: for c st c in Class EqR holds y.c = F(c) from MSSLambda; A6: U2' = SORTS(product (A/EqR)) by PRALG_2:20; take y; y in product Carrier(product (A/EqR),s') proof A7: dom Carrier(product (A/EqR),s') = Class EqR by PBOOLE:def 3 .= dom y by PBOOLE:def 3; A8: dom Carrier(product (A/EqR),s') = Class EqR by PBOOLE:def 3; for a be set st a in dom (Carrier(product (A/EqR),s')) holds y.a in (Carrier(product (A/EqR),s')).a proof let a be set such that A9: a in dom (Carrier(product (A/EqR),s')); set A' = product (A/EqR); A10: (A/EqR).a = A|a by A8,A9,Def5; consider b be set such that A11: b in I and A12: a = Class(EqR,b) by A8,A9,EQREL_1:def 5; reconsider a as non empty Subset of I by A11,A12,EQREL_1:28; A13:dom (A|a) = dom A /\ a by RELAT_1:90 .= I /\ a by PBOOLE:def 3 .= a by XBOOLE_1:28; then reconsider Aa1 = A|a as ManySortedSet of a by PBOOLE:def 3; for i be set st i in a holds Aa1.i is non-empty MSAlgebra over S proof let i be set; assume A14: i in a; then A.i is non-empty MSAlgebra over S by PRALG_2:def 12; hence thesis by A13,A14,FUNCT_1:70; end; then reconsider Aa = Aa1 as MSAlgebra-Family of a,S by PRALG_2:def 12; x|a in product((Carrier(A,s'))|a) by A3,A4,Th1; then A15: x|a in product (Carrier(Aa,s')) by Th2; consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such that A16: Ji = (id Class EqR).a and A17: Cs = (A/EqR).a and A18: A'.a = product Cs by A8,A9,Def6; A19: Ji = a by A8,A9,A16,FUNCT_1:35; consider U0 being MSAlgebra over S such that A20:U0 = A'.a & (Carrier(A',s')).a = (the Sorts of U0).s' by A8,A9,PRALG_2:def 16; (Carrier(A',s')).a = (SORTS Cs).s' by A18,A20,PRALG_2:20 .= product (Carrier(Aa,s')) by A10,A17,A19,PRALG_2:def 17; hence thesis by A5,A8,A9,A15; end; hence thesis by A7,CARD_3:18; end; hence thesis by A5,A6,PRALG_2:def 17; end; consider F be ManySortedFunction of U1', U2' such that A21: for s be set st s in the carrier of S holds ex f be Function of U1'.s, U2'.s st f = F.s & for x be set st x in U1'.s holds P[f.x,x,s] from MSFExFunc(A1); A22: F is_homomorphism U1,U2 proof let o be OperSymbol of S such that Args(o,U1) <> {}; let x be Element of Args(o,U1); thus (F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,U2).(F#x) proof set s = the_result_sort_of o, U3 = product (A/EqR); consider f be Function of U1'.s, U2'.s such that A23: f = F.s and A24: for x' be set st x' in U1'.s holds P[f.x',x',s] by A21; A25:U2'.s = (SORTS U3).s by PRALG_2:20 .= product Carrier(U3,s) by PRALG_2:def 17; A26:dom (F.s) = U1'.s by FUNCT_2:def 1 .= (SORTS A).s by PRALG_2:20 .= product Carrier(A,s) by PRALG_2:def 17; A27:Den(o,U1).x in Result(o,U1); then A28: Den(o,U1).x in U1'.(the_result_sort_of o) by PRALG_2:10; A29:Den(o,U1).x in product Carrier(A,s) by Th20; per cases; suppose A30:the_arity_of o = {}; then Args(o,U1) = {{}} by PRALG_2:11; then A31: x = {} by TARSKI:def 1; then const(o,U1) in Result(o,U1) by A27,Def1; then A32:const(o,U1) in U1'.(the_result_sort_of o) by PRALG_2:10; A33:const(o,U1) in product Carrier(A,s) by A29,A31,Def1; then A34: dom (const(o,U1)) = dom Carrier(A,s) by CARD_3:18 .= I by PBOOLE:def 3; A35: F.s.const(o,U1) in rng (F.s) by A26,A33,FUNCT_1:def 5; then reconsider g1 = F.s.const(o,U1) as Function by A25,Lm1; A36:dom g1 = dom (Carrier(U3,s)) by A25,A35,CARD_3:18 .= Class EqR by PBOOLE:def 3; const(o,U2) in Funcs(Class EqR, union { Result(o,U3.i') where i' is Element of Class EqR: not contradiction }) by A30,Th9; then A37:dom const(o,U2) = Class EqR by Th4; A38:now let e be Element of Class EqR; consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such that A39: Ji = (id Class EqR).e & Cs = (A/EqR).e & U3.e = product Cs by Def6; A40: dom (const(o,product A)|e) = I /\ e by A34,RELAT_1:90 .= e by XBOOLE_1:28; const(o,product Cs) in Funcs(Ji, union { Result(o,Cs.i') where i' is Element of Ji: not contradiction }) by A30,Th9; then A41: dom (const(o,product Cs)) = Ji by Th4 .= e by A39,FUNCT_1:35; now let i1 be set; assume A42: i1 in e; then reconsider ii = i1 as Element of Ji by A39,FUNCT_1:35; reconsider ii' = ii as Element of I by A42; A43: dom(A|e) = dom A /\ e by RELAT_1:90 .= I /\ e by PBOOLE:def 3 .= e by XBOOLE_1:28; Cs = A|e by A39,Def5; then A44: Cs.ii = A.ii' by A42,A43,FUNCT_1:70; thus (const(o,product A)|e).i1 = const(o,product A).i1 by A40,A42,FUNCT_1:70 .= const(o,A.ii') by A30,Th10 .= const(o,product Cs).i1 by A30,A44,Th10; end; hence const(o,U1)|e = const(o,U3.e) by A39,A40,A41,FUNCT_1:9; end; now let x1 be set; assume x1 in Class EqR; then reconsider e = x1 as Element of Class EqR; consider f1 be Function such that A45: f1 = const(o,U1); g1.e = f1|e by A23,A24,A32,A45; hence g1.x1 = const(o,U3.e) by A38,A45 .= const(o,product U3).x1 by A30,Th10; end; then A46: F.s.const(o,U1) = const(o,U2) by A36,A37,FUNCT_1:9; thus Den(o,U2).(F#x) = Den(o,U2).{} by A30,A31,Th12 .= F.s.const(o,U1) by A46,Def1 .= (F.(the_result_sort_of o)).(Den(o,U1).x) by A31,Def1; suppose A47:the_arity_of o <> {}; A48: (F.s).(Den(o,U1).x) in rng (F.s) by A26,A29,FUNCT_1:def 5; then reconsider g1 = (F.s).(Den(o,U1).x) as Function by A25,Lm1; A49:Den(o,U2).(F#x) in product Carrier(U3,s) by Th20; then reconsider f1 = Den(o,U2).(F#x) as Function by Lm1; A50: dom g1 = dom (Carrier(U3,s)) by A25,A48,CARD_3:18 .= Class EqR by PBOOLE:def 3; A51: dom f1 = dom (Carrier(U3,s)) by A49,CARD_3:18 .= Class EqR by PBOOLE:def 3; A52:now let e be Element of Class EqR; let f2 be Function such that A53: f2 = Den(o,U1).x; consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such that A54: Ji = (id Class EqR).e & Cs = (A/EqR).e & U3.e = product Cs by Def6; dom f2 = dom (Carrier(A,s)) by A29,A53,CARD_3:18 .= I by PBOOLE:def 3; then A55: dom (f2|e) = I /\ e by RELAT_1:90 .= e by XBOOLE_1:28; A56: (commute (F#x)).e is Element of Args(o,U3.e) by A47,Th21; A57:(commute (F#x)).e is Element of Args(o,product Cs) by A47,A54,Th21; A58:Den(o,U3.e).((commute (F#x)).e) in product Carrier(Cs,s) by A54,A56,Th20; then reconsider f3 = Den(o,U3.e).((commute (F#x)).e) as Function by Lm1; A59: dom f3 = dom (Carrier(Cs,s)) by A58,CARD_3:18 .= Ji by PBOOLE:def 3 .= e by A54,FUNCT_1:35; A60: now let i1 be Element of I; assume A61: i1 in e; then reconsider i2 = i1 as Element of Ji by A54,FUNCT_1:35; (commute ((commute (F#x)).e)).i2 is Element of Args(o,Cs.i2) by A47,A54,A56,Th21; then (commute ((commute (F#x)).e)).i2 in Args(o,Cs.i2); then (commute ((commute (F#x)).e)).i2 in product ((the Sorts of Cs.i2)*(the_arity_of o)) by PRALG_2:10; then A62: dom ((commute ((commute (F#x)).e)).i1) = dom ((the Sorts of Cs.i2)*(the_arity_of o)) by CARD_3:18 .= dom (the_arity_of o) by PRALG_2:10; (commute x).i1 is Element of Args(o,A.i1) by A47,Th21; then (commute x).i1 in Args(o,A.i1); then (commute x).i1 in product ((the Sorts of A.i1)*(the_arity_of o)) by PRALG_2:10; then A63:dom ((commute x).i1) = dom ((the Sorts of A.i1)*(the_arity_of o)) by CARD_3:18 .= dom (the_arity_of o) by PRALG_2:10; now let n be set; assume A64:n in dom (the_arity_of o); then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 5; then reconsider s1 = (the_arity_of o).n as SortSymbol of S; A65: x.n in product Carrier(A,(the_arity_of o)/.n) by A64,Th16; then A66:x.n in product Carrier(A,s1) by A64,FINSEQ_4:def 4; reconsider f4 = x.n as Function by A65,Lm1; x.n in (SORTS A).s1 by A66,PRALG_2:def 17; then A67:x.n in U1'.s1 by PRALG_2:20; dom f4 = dom (Carrier(A,s1)) by A66,CARD_3:18 .= I by PBOOLE:def 3; then A68:dom (f4|e) = I /\ e by RELAT_1:90 .= e by XBOOLE_1:28; (F#x).n in product Carrier (U3,(the_arity_of o)/.n) by A64,Th16; then reconsider f5 = (F#x).n as Function by Lm1; consider f7 be Function of U1'.s1, U2'.s1 such that A69: f7 = F.s1 and A70: for x' be set st x' in U1'.s1 holds P[f7.x',x',s1] by A21; f5 = F.((the_arity_of o)/.n).(x.n) by A64,Th14 .= f7.(x.n) by A64,A69,FINSEQ_4:def 4; then A71:f5.e = f4|e by A67,A70; then reconsider f6 = f5.e as Function; f6 = ((commute (F#x)).e).n by A64,Th22; hence ((commute((commute (F#x)).e)).i1).n = (f4|e).i2 by A54,A56,A64,A71,Th22 .= f4.i2 by A61,A68,FUNCT_1:70 .= ((commute x).i1).n by A64,Th22; end; hence ((commute ((commute (F#x)).e)).i1) = ((commute x).i1) by A62,A63,FUNCT_1:9; end; now let x1 be set; assume A72: x1 in e; then reconsider i2 = x1 as Element of Ji by A54,FUNCT_1:35; reconsider i1 = i2 as Element of I by A72; A73: dom(A|e) = dom A /\ e by RELAT_1:90 .= I /\ e by PBOOLE:def 3 .= e by XBOOLE_1:28; Cs = A|e by A54,Def5; then Cs.i2 = A.i1 by A72,A73,FUNCT_1:70; hence f3.x1 = Den(o,A.i1).((commute ((commute (F#x)).e)).i2) by A47,A54,A57, Th23 .= Den(o,A.i1).((commute x).i1) by A60,A72 .= f2.x1 by A47,A53,Th23 .= (f2|e).x1 by A55,A72,FUNCT_1:70; end; hence f2|e = Den(o,U3.e).((commute (F#x)).e) by A55,A59,FUNCT_1:9; end; now let x1 be set; assume x1 in Class EqR; then reconsider e = x1 as Element of Class EqR; reconsider f2 = Den(o,U1).x as Function by A29,Lm1; g1.e = f2|e by A23,A24,A28; hence g1.x1 = Den(o,U3.e).((commute (F#x)).e) by A52 .= f1.x1 by A47,Th23; end; hence (F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,U2).(F#x) by A50, A51,FUNCT_1:9; end; end; A74: F is "onto" proof let s be set such that A75: s in the carrier of S; reconsider s' = s as SortSymbol of S by A75; U1' = SORTS A by PRALG_2:20; then A76: U1'.s' = product Carrier(A,s') by PRALG_2:def 17; A77: U2' = SORTS(product (A/EqR)) by PRALG_2:20; A78: U2'.s' is non empty set; consider f be Function of U1'.s, U2'.s such that A79: f = F.s and A80: for x be set st x in U1'.s holds P[f.x,x,s] by A21,A75; for y be set holds y in (U2'.s) iff ex x be set st x in dom f & y = f.x proof let y be set; thus y in (U2'.s) iff ex x be set st x in dom f & y = f.x proof thus y in (U2'.s) implies ex x be set st x in dom f & y = f.x proof assume y in (U2'.s); then A81: y in product Carrier(product (A/EqR),s') by A77,PRALG_2:def 17; then consider gg be Function such that A82: y = gg & dom gg = dom (Carrier(product (A/EqR),s')) and A83: for x' be set st x' in dom (Carrier(product (A/EqR),s')) holds gg.x' in (Carrier(product (A/EqR),s')).x' by CARD_3:def 5; reconsider y as Function by A81,Lm1; A84: dom Carrier(product (A/EqR),s') = Class EqR by PBOOLE:def 3; defpred Q[set,set] means ex e being Element of Class EqR, f being Function st $1 in e & f = y.e & $2 = f.$1; A85: for i be set st i in I ex j being set st Q[i,j] proof let i be set such that A86: i in I; A87: dom (Carrier(product (A/EqR),s')) = Class EqR by PBOOLE:def 3; Class(EqR,i) in Class EqR by A86,EQREL_1:def 5; then consider e be Element of Class EqR such that A88: e = Class(EqR,i); A89: gg.e in (Carrier(product (A/EqR),s')).e by A83,A87; consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such that Ji = (id Class EqR).e and Cs = (A/EqR).e and A90: (product (A/EqR)).e = product Cs by Def6; consider U0 being MSAlgebra over S such that A91:U0 = (product (A/EqR)).e & (Carrier(product (A/EqR),s')).e = (the Sorts of U0).s' by PRALG_2:def 16; (Carrier(product (A/EqR),s')).e = (SORTS Cs).s' by A90,A91,PRALG_2:20 .= product Carrier(Cs,s') by PRALG_2:def 17; then reconsider y' = y.e as Function by A82,A89,Lm1; Q[i,y'.i] proof take e; reconsider f=y' as Function; take f; thus thesis by A86,A88,EQREL_1:28; end; hence thesis; end; consider x being ManySortedSet of I such that A92: for i be set st i in I holds Q[i,x.i] from MSSEx(A85); A93: x in U1'.s' proof A94: dom x = I by PBOOLE:def 3 .= dom Carrier(A,s') by PBOOLE:def 3; for z be set st z in dom Carrier(A,s') holds x.z in (Carrier(A,s')).z proof let z be set; assume z in dom Carrier(A,s'); then z in I by PBOOLE:def 3; then consider e being Element of Class EqR,f1 being Function such that A95: z in e & f1 = y.e and A96: x.z = f1.z by A92; A97: y.e in (Carrier(product (A/EqR),s')).e by A82,A83,A84; consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such that A98: Ji = (id Class EqR).e and A99: Cs = (A/EqR).e and A100: (product (A/EqR)).e = product Cs by Def6; consider U0 being MSAlgebra over S such that A101:U0 = (product (A/EqR)).e & (Carrier(product (A/EqR),s')).e = (the Sorts of U0).s' by PRALG_2:def 16; (Carrier(product (A/EqR),s')).e = (SORTS Cs).s' by A100,A101,PRALG_2:20 .= product Carrier(Cs,s') by PRALG_2:def 17; then consider g be Function such that A102: y.e = g & dom g = dom Carrier(Cs,s') and A103: for x' be set st x' in dom Carrier(Cs,s') holds g.x' in (Carrier(Cs,s')).x' by A97,CARD_3:def 5; dom ((Carrier(A,s'))|e) = dom Carrier(A,s') /\ e by RELAT_1:90 .= I /\ e by PBOOLE:def 3 .= e by XBOOLE_1:28; then A104: ((Carrier(A,s'))|e).z = (Carrier(A,s')).z by A95,FUNCT_1:70; A105: Cs = A|e by A99,Def5; Ji = e by A98,FUNCT_1:35; then A106: Carrier(Cs,s') = (Carrier(A,s'))|e by A105,Th2; dom Carrier(Cs,s') = Ji by PBOOLE:def 3 .= e by A98,FUNCT_1:35; hence thesis by A95,A96,A102,A103,A104,A106; end; hence thesis by A76,A94,CARD_3:18; end; then A107: x in dom f by A78,FUNCT_2:def 1; then f.x in rng f by FUNCT_1:def 5; then f.x in U2'.s; then f.x in product Carrier(product (A/EqR),s') by A77,PRALG_2:def 17; then consider gg' be Function such that A108: f.x = gg' & dom gg' = dom (Carrier(product (A/EqR),s')) and for x' be set st x' in dom (Carrier(product (A/EqR),s')) holds gg'.x' in (Carrier(product (A/EqR),s')).x' by CARD_3:def 5; reconsider f' = f.x as Function by A108; y = f' proof for e be set st e in Class EqR holds y.e = f'.e proof let e be set; assume e in Class EqR; then reconsider e as Element of Class EqR; A109: y.e in (Carrier(product (A/EqR),s')).e by A82,A83,A84; consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such that A110: Ji = (id Class EqR).e and Cs = (A/EqR).e and A111: (product (A/EqR)).e = product Cs by Def6; consider U0 being MSAlgebra over S such that A112:U0 = (product (A/EqR)).e & (Carrier(product (A/EqR),s')).e = (the Sorts of U0).s' by PRALG_2:def 16; (Carrier(product (A/EqR),s')).e = (SORTS Cs).s' by A111,A112,PRALG_2:20 .= product Carrier(Cs,s') by PRALG_2:def 17; then consider g be Function such that A113: y.e = g & dom g = dom Carrier(Cs,s') and for x' be set st x' in dom Carrier(Cs,s') holds g.x' in (Carrier(Cs,s')).x' by A109,CARD_3:def 5; reconsider y' = y.e as Function by A113; x|e = y' proof A114: dom (x|e) = dom x /\ e by RELAT_1:90 .= I /\ e by PBOOLE:def 3 .= e by XBOOLE_1:28; A115: dom y' = Ji by A113,PBOOLE:def 3 .= e by A110,FUNCT_1:35; for i be set st i in e holds (x|e).i = y'.i proof let i be set; assume A116: i in e; then consider e1 being Element of Class EqR,f1 being Function such that A117: i in e1 and A118: f1 = y.e1 and A119: x.i = f1.i by A92; e = e1 by A116,A117,Th3; hence thesis by A114,A116,A118,A119,FUNCT_1:70; end; hence thesis by A114,A115,FUNCT_1:9; end; hence thesis by A80,A93; end; hence thesis by A82,A84,A108,FUNCT_1:9; end; hence thesis by A107; end; thus (ex x be set st x in dom f & y = f.x) implies y in (U2'.s) proof given x be set such that A120: x in dom f and A121: y = f.x; f.x in rng f by A120,FUNCT_1:def 5; hence thesis by A121; end; end; end; hence rng(F.s) = U2'.s by A79,FUNCT_1:def 5; end; A122:F is "1-1" proof let s be set, g be Function such that A123: s in dom F & F.s = g; let x1,x2 be set such that A124: x1 in dom g and A125: x2 in dom g and A126: g.x1 = g.x2; dom F = the carrier of S by PBOOLE:def 3; then consider f being Function of U1'.s, U2'.s such that A127: f = F.s and A128: for x be set st x in U1'.s holds P[f.x,x,s] by A21,A123; A129: dom f = dom g by A123,A127; thus x1 = x2 proof reconsider s' = s as SortSymbol of S by A123,PBOOLE:def 3; U1' = SORTS A by PRALG_2:20; then A130: U1'.s' = product Carrier(A,s') by PRALG_2:def 17; U2' = SORTS(product (A/EqR)) by PRALG_2:20; then A131: U2'.s = product Carrier(product (A/EqR),s') by PRALG_2:def 17; A132: U2'.s' is non empty set; consider gg be Function such that A133: x1 = gg and A134: dom gg = dom Carrier(A,s') and for x' be set st x' in dom Carrier(A,s') holds gg.x' in (Carrier(A,s')).x' by A124,A129,A130,CARD_3:def 5; reconsider x1 as Function by A133; consider gg1 be Function such that A135: x2 = gg1 and A136: dom gg1 = dom Carrier(A,s') and for x' be set st x' in dom Carrier(A,s') holds gg1.x' in (Carrier(A,s')).x' by A125,A129,A130,CARD_3:def 5; reconsider x2 as Function by A135; A137: dom x1 = I by A133,A134,PBOOLE:def 3; A138: dom x2 = I by A135,A136,PBOOLE:def 3; for i be set st i in I holds x1.i = x2.i proof let i be set; assume A139: i in I; then A140: i in Class(EqR,i) by EQREL_1:28; A141: Class(EqR,i) is Element of Class EqR by A139,EQREL_1:def 5; f.x2 in U2'.s by A125,A129,A132,FUNCT_2:7; then reconsider f'' = f.x2 as Function by A131,Lm1; x1|(Class(EqR,i)) = f''.(Class(EqR,i)) by A123,A124,A126,A127,A128,A129, A141 .= x2|(Class(EqR,i)) by A125,A128,A129,A141; then x1.i = (x2|(Class(EqR,i))).i by A140,FUNCT_1:72 .= x2.i by A140,FUNCT_1:72; hence thesis; end; hence thesis by A137,A138,FUNCT_1:9; end; end; F is_isomorphism U1,U2 proof thus F is_epimorphism U1,U2 proof thus F is_homomorphism U1,U2 & F is "onto" by A22,A74; end; thus F is_monomorphism U1,U2 proof thus F is_homomorphism U1,U2 & F is "1-1" by A22,A122; end; end; hence thesis by MSUALG_3:def 13; end;

Back to top