### The Mizar article:

### Product of Family of Universal Algebras

**by****Beata Madras**

- Received October 12, 1993
Copyright (c) 1993 Association of Mizar Users

- MML identifier: PRALG_1
- [ MML identifier index ]

environ vocabulary FINSEQ_2, FINSEQ_1, UNIALG_1, FUNCT_3, RELAT_1, FUNCT_1, MCART_1, FUNCT_2, PARTFUN1, TARSKI, CQC_SIM1, UNIALG_2, BOOLE, ZF_REFLE, FINSEQ_4, ORDINAL2, PBOOLE, FUNCOP_1, RLVECT_2, CARD_3, FUNCT_5, PRALG_1, ARYTM; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, NAT_1, STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, FUNCT_2, FUNCOP_1, MCART_1, DOMAIN_1, PARTFUN1, FINSEQ_2, FUNCT_4, FUNCT_5, CARD_3, DTCONSTR, UNIALG_1, UNIALG_2, PBOOLE; constructors DOMAIN_1, FRAENKEL, FUNCT_4, FUNCT_5, CARD_3, DTCONSTR, UNIALG_2, PBOOLE, MEMBERED, XBOOLE_0; clusters SUBSET_1, UNIALG_1, PRVECT_1, PBOOLE, FUNCT_1, RELAT_1, RELSET_1, STRUCT_0, FINSEQ_2, PARTFUN1, FUNCOP_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET; definitions TARSKI, UNIALG_1, UNIALG_2, FUNCT_1, PBOOLE, XBOOLE_0; theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, FUNCOP_1, UNIALG_1, DOMAIN_1, ZFMISC_1, MCART_1, UNIALG_2, FUNCT_2, PBOOLE, FUNCT_5, CARD_3, FUNCT_4, FINSEQ_3, RELAT_1, RELSET_1, DTCONSTR, STRUCT_0, ORDINAL2, XBOOLE_0, XBOOLE_1; schemes MATRIX_2, PARTFUN1, FUNCT_2, FUNCT_1, ZFREFLE1, COMPTS_1; begin theorem Th1: for D1,D2 be non empty set,n,m be Nat st n-tuples_on D1 = m-tuples_on D2 holds n = m proof let D1,D2 be non empty set,n,m be Nat; assume A1: n-tuples_on D1 = m-tuples_on D2; consider p be Element of n-tuples_on D1; p in m-tuples_on D2 by A1; then p in {w where w is Element of D2* : len w = m} by FINSEQ_2:def 4; then consider w be Element of D2* such that A2: p = w & len w = m; thus m = n by A2,FINSEQ_2:109; end; :: :: Product of Two Algebras :: reserve U1,U2,U3 for Universal_Algebra, k,n,m,i for Nat, x,y,z for set, A,B for non empty set, h1 for FinSequence of [:A,B:]; definition let A,B; let h1; redefine func pr1 h1 -> FinSequence of A means :Def1: len it = len h1 & for n st n in dom it holds it.n = (h1.n)`1; compatibility proof let f1 be FinSequence of A; hereby assume A1: f1 = pr1 h1; then A2: dom f1 = dom h1 by DTCONSTR:def 2; hence len f1 = len h1 by FINSEQ_3:31; let n; thus n in dom f1 implies f1.n = (h1.n)`1 by A1,A2,DTCONSTR:def 2; end; assume that A3: len f1 = len h1 and A4: for n st n in dom f1 holds f1.n = (h1.n)`1; dom f1 = dom h1 & for n being set st n in dom f1 holds f1.n = (h1.n)`1 by A3,A4,FINSEQ_3:31; hence thesis by DTCONSTR:def 2; end; coherence proof thus pr1 h1 is FinSequence of A; end; func pr2 h1 -> FinSequence of B means :Def2: len it = len h1 & for n st n in dom it holds it.n = (h1.n)`2; compatibility proof let f1 be FinSequence of B; hereby assume A5: f1 = pr2 h1; then A6: dom f1 = dom h1 by DTCONSTR:def 3; hence len f1 = len h1 by FINSEQ_3:31; let n; thus n in dom f1 implies f1.n = (h1.n)`2 by A5,A6,DTCONSTR:def 3; end; assume that A7: len f1 = len h1 and A8: for n st n in dom f1 holds f1.n = (h1.n)`2; dom f1 = dom h1 & for n being set st n in dom f1 holds f1.n = (h1.n)`2 by A7,A8,FINSEQ_3:31; hence thesis by DTCONSTR:def 3; end; coherence proof thus pr2 h1 is FinSequence of B; end; end; definition let A,B; let f1 be homogeneous quasi_total non empty PartFunc of A*,A; let f2 be homogeneous quasi_total non empty PartFunc of B*,B; assume A1: arity (f1) = arity (f2); func [[:f1,f2:]] -> homogeneous quasi_total non empty PartFunc of ([:A,B:])*,[:A,B:] means :Def3: dom it = (arity(f1))-tuples_on [:A,B:] & for h be FinSequence of [:A,B:] st h in dom it holds it.h = [f1.(pr1 h),f2.(pr2 h)]; existence proof defpred P[set,set] means for h be FinSequence of [:A,B:] st $1 = h holds $2 = [f1.(pr1 h),f2.(pr2 h)]; set ar = (arity(f1))-tuples_on [:A,B:], ab = {s where s is Element of [:A,B:]* : len s = arity(f1)}; A2: dom f1 = (arity(f1))-tuples_on A by UNIALG_2:2; A3: dom f2 = (arity(f2))-tuples_on B by UNIALG_2:2; A4: rng f1 c= A by RELSET_1:12; A5: rng f2 c= B by RELSET_1:12; A6: for x,y st x in ar & P[x,y] holds y in [:A,B:] proof let x,y; assume A7: x in ar & P[x,y]; then x in ab by FINSEQ_2:def 4; then consider s being Element of [:A,B:]* such that A8: x = s & len s = arity(f1); A9: y = [f1.(pr1 s),f2.(pr2 s)] by A7,A8; A10: len pr1 s = len s & len pr2 s = len s by Def1,Def2; reconsider s1 = pr1 s as Element of A* by FINSEQ_1:def 11; reconsider s2 = pr2 s as Element of B* by FINSEQ_1:def 11; s1 in {s3 where s3 is Element of A* : len s3 = arity(f1)} by A8,A10; then s1 in dom f1 by A2,FINSEQ_2:def 4; then A11: f1.s1 in rng f1 by FUNCT_1:def 5; s2 in {s3 where s3 is Element of B* : len s3 = arity(f2)} by A1,A8,A10; then s2 in dom f2 by A3,FINSEQ_2:def 4; then f2.s2 in rng f2 by FUNCT_1:def 5 ; hence thesis by A4,A5,A9,A11,ZFMISC_1:106; end; A12: for x,y,z st x in ar & P[x,y] & P[x,z] holds y = z proof let x,y,z; assume A13: x in ar & P[x,y] & P[x,z]; then x in ab by FINSEQ_2:def 4; then consider s being Element of [:A,B:]* such that A14: x = s & len s = arity(f1); y = [f1.(pr1 s),f2.(pr2 s)] & z = [f1.(pr1 s),f2.(pr2 s)] by A13,A14; hence thesis; end; consider f being PartFunc of ar,[:A,B:] such that A15: for x holds x in dom f iff x in ar & ex y st P[x,y] and A16: for x st x in dom f holds P[x,f.x] from PartFuncEx(A6,A12); A17: dom f = ar proof thus dom f c= ar proof let x; assume x in dom f; hence thesis by A15; end; let x; assume A18: x in ar; then x in ab by FINSEQ_2:def 4; then consider s being Element of [:A,B:]* such that A19: x = s & len s = arity f1; now take y = [f1.(pr1 s),f2.(pr2 s)]; let h be FinSequence of [:A,B:]; assume h = x; hence y = [f1.(pr1 h),f2.(pr2 h)] by A19; end; hence thesis by A15,A18; end; ar in {i-tuples_on [:A,B:]: not contradiction}; then ar c= union{i-tuples_on [:A,B:]: not contradiction} by ZFMISC_1:92; then ar c= [:A,B:]* by FINSEQ_2:128; then reconsider f as PartFunc of [:A,B:]*,[:A,B:] by PARTFUN1:30; A20: f is homogeneous proof let x,y be FinSequence of [:A,B:]; assume x in dom f & y in dom f; then A21: x in ab & y in ab by A17,FINSEQ_2:def 4; then consider s1 being Element of [:A,B:]* such that A22: s1 = x & len s1 = arity(f1); consider s2 being Element of [:A,B:]* such that A23: s2 = y & len s2 = arity(f1) by A21; thus thesis by A22,A23; end; f is quasi_total proof let x,y be FinSequence of [:A,B:]; assume A24: len x = len y & x in dom f; then x in ab by A17,FINSEQ_2:def 4; then consider s1 being Element of [:A,B:]* such that A25: s1 = x & len s1 = arity(f1); reconsider y' = y as Element of [:A,B:]* by FINSEQ_1:def 11; y' in ab by A24,A25; hence thesis by A17,FINSEQ_2:def 4; end; then reconsider f as homogeneous quasi_total non empty PartFunc of ([:A,B:])*,[:A,B:] by A17,A20,UNIALG_1:1; take f; thus dom f = ar by A17; let h be FinSequence of [:A,B:]; assume h in dom f; hence thesis by A16; end; uniqueness proof let x,y be homogeneous quasi_total non empty PartFunc of ([:A,B:])* ,[:A,B:]; assume that A26: dom x = (arity(f1))-tuples_on [:A,B:] and A27: for h be FinSequence of [:A,B:] st h in dom x holds x.h = [f1.(pr1 h),f2.(pr2 h)] and A28: dom y = (arity(f1))-tuples_on [:A,B:] and A29: for h be FinSequence of [:A,B:] st h in dom y holds y.h = [f1.(pr1 h),f2.(pr2 h)]; now let c be Element of [:A,B:]*; reconsider c' = c as FinSequence of [:A,B:]; assume c in dom x; then x.c' = [f1.(pr1 c'),f2.(pr2 c')] & y.c' = [f1.(pr1 c'),f2.(pr2 c')] by A26,A27,A28,A29; hence x.c = y.c; end; hence thesis by A26,A28,PARTFUN1:34; end; end; reserve h1 for homogeneous quasi_total non empty PartFunc of (the carrier of U1)*,the carrier of U1, h2 for homogeneous quasi_total non empty PartFunc of (the carrier of U2)*,the carrier of U2; definition let U1,U2; assume A1: U1,U2 are_similar; func Opers(U1,U2) -> PFuncFinSequence of [:the carrier of U1,the carrier of U2:] means :Def4: len it = len the charact of(U1) & for n st n in dom it holds for h1,h2 st h1=(the charact of(U1)).n & h2=(the charact of(U2)).n holds it.n = [[:h1,h2:]]; existence proof set l = len the charact of(U1), c = [:the carrier of U1,the carrier of U2:]; A2: Seg l = dom the charact of(U1) & dom the charact of(U2) = Seg len the charact of(U2) by FINSEQ_1:def 3; defpred P[Nat,set] means for h1,h2 st h1=(the charact of(U1)).$1 & h2=(the charact of(U2)).$1 holds $2 = [[:h1,h2:]]; A3: for m st m in Seg l ex x being Element of PFuncs(c*,c) st P[m,x] proof let m; assume A4: m in Seg l; then reconsider f1 = (the charact of(U1)).m as homogeneous quasi_total non empty PartFunc of (the carrier of U1)*,the carrier of U1 by A2,UNIALG_1:5,def 4,def 5,def 6; len the charact of(U1) = len the charact of(U2) by A1,UNIALG_2:3; then reconsider f2 = (the charact of(U2)).m as homogeneous quasi_total non empty PartFunc of (the carrier of U2)*,the carrier of U2 by A2,A4,UNIALG_1:5,def 4,def 5,def 6; reconsider F = [[:f1,f2:]] as Element of PFuncs(c*,c) by PARTFUN1:119; take F; let h1,h2; assume h1=(the charact of(U1)).m & h2=(the charact of(U2)).m; hence F = [[:h1,h2:]]; end; consider p be FinSequence of PFuncs(c*,c) such that A5: dom p = Seg l and A6: for m st m in Seg l holds P[m,p.m] from SeqDEx(A3); reconsider p as PFuncFinSequence of c; take p; thus len p = len the charact of(U1) by A5,FINSEQ_1:def 3; let n; assume n in dom p; hence thesis by A5,A6; end; uniqueness proof let x,y be PFuncFinSequence of [:the carrier of U1,the carrier of U2:]; assume that A7: len x = len the charact of(U1) and A8:for n st n in dom x holds for h1,h2 st h1=(the charact of(U1)).n & h2=(the charact of(U2)).n holds x.n = [[:h1,h2:]] and A9: len y = len the charact of(U1) and A10:for n st n in dom y holds for h1,h2 st h1=(the charact of(U1)).n & h2=(the charact of(U2)).n holds y.n = [[:h1,h2:]]; now let m; assume A11: m in Seg len the charact of(U1); Seg len the charact of(U2) = Seg len the charact of(U1) by A1,UNIALG_2:3; then A12: m in dom the charact of(U1) & m in dom the charact of(U2) & m in dom x & m in dom y by A7,A9,A11,FINSEQ_1:def 3; then reconsider h1=(the charact of(U1)).m as homogeneous quasi_total non empty PartFunc of (the carrier of U1)*,the carrier of U1 by UNIALG_1:5,def 4,def 5,def 6; reconsider h2=(the charact of(U2)).m as homogeneous quasi_total non empty PartFunc of (the carrier of U2)*,the carrier of U2 by A12,UNIALG_1:5,def 4,def 5,def 6; x.m = [[:h1,h2:]] & y.m = [[:h1,h2:]] by A8,A10,A12; hence x.m = y.m; end; hence thesis by A7,A9,FINSEQ_2:10; end; end; theorem Th2: U1,U2 are_similar implies UAStr (# [:the carrier of U1,the carrier of U2:], Opers(U1,U2) #) is strict Universal_Algebra proof assume A1: U1,U2 are_similar; set C = UAStr(# [:the carrier of U1,the carrier of U2:], Opers(U1,U2) #); A2: dom Opers(U1,U2) = Seg len Opers(U1,U2) & dom the charact of(U1) = Seg len the charact of(U1) & dom the charact of(U2) = Seg len the charact of(U2) by FINSEQ_1:def 3; A3: len Opers(U1,U2) = len the charact of(U1) & len the charact of(U2) = len the charact of(U1) by A1,Def4,UNIALG_2:3; A4: the charact of(C) is quasi_total proof let n; let h be PartFunc of (the carrier of C)*,(the carrier of C); assume A5: n in dom the charact of(C) & h = (the charact of(C)).n; then reconsider h1=(the charact of U1).n as homogeneous quasi_total non empty PartFunc of (the carrier of U1)*,the carrier of U1 by A2,A3,UNIALG_1:5,def 4,def 5,def 6; reconsider h2=(the charact of(U2)).n as homogeneous quasi_total non empty PartFunc of (the carrier of U2)*,the carrier of U2 by A2,A3,A5,UNIALG_1:5,def 4,def 5,def 6; h = [[:h1,h2:]] by A1,A5,Def4; hence h is quasi_total; end; A6: the charact of(C) is homogeneous proof let n; let h be PartFunc of (the carrier of C)*,the carrier of C; assume A7: n in dom the charact of(C) & h = (the charact of(C)).n; then reconsider h1=(the charact of(U1)).n as homogeneous quasi_total non empty PartFunc of (the carrier of U1)*,the carrier of U1 by A2,A3,UNIALG_1:5,def 4,def 5,def 6; reconsider h2=(the charact of(U2)).n as homogeneous quasi_total non empty PartFunc of (the carrier of U2)*,the carrier of U2 by A2,A3,A7,UNIALG_1:5,def 4,def 5,def 6; h = [[:h1,h2:]] by A1,A7,Def4; hence h is homogeneous; end; A8: the charact of(C) <> {} proof assume the charact of(C) = {}; then len the charact of(C) = 0 by FINSEQ_1:25; hence contradiction by A3,FINSEQ_1:25; end; the charact of(C) is non-empty proof let n be set; set h = (the charact of(C)).n; assume A9: n in dom the charact of(C); then reconsider m = n as Nat; reconsider h1=(the charact of(U1)).m as homogeneous quasi_total non empty PartFunc of (the carrier of U1)*,the carrier of U1 by A2,A3,A9,UNIALG_1:5,def 4,def 5,def 6; reconsider h2=(the charact of(U2)).m as homogeneous quasi_total non empty PartFunc of (the carrier of U2)*,the carrier of U2 by A2,A3,A9,UNIALG_1:5,def 4,def 5,def 6; h = [[:h1,h2:]] by A1,A9,Def4; hence h is non empty; end; hence thesis by A4,A6,A8,UNIALG_1:def 7,def 8,def 9; end; definition let U1,U2; assume A1: U1,U2 are_similar; func [:U1,U2:] -> strict Universal_Algebra equals :Def5: UAStr (# [:the carrier of U1,the carrier of U2:], Opers(U1,U2) #); coherence by A1,Th2; end; definition let A,B be non empty set; func Inv (A,B) -> Function of [:A,B:],[:B,A:] means :Def6: for a be Element of [:A,B:] holds it.a = [a`2,a`1]; existence proof deffunc F(Element of [:A,B:]) = [$1`2,$1`1]; thus ex I be Function of [:A,B:],[:B,A:] st for a be Element of [:A,B:] holds I.a = F(a) from LambdaD; end; uniqueness proof let f,g be Function of [:A,B:],[:B,A:]; assume A1: (for a be Element of [:A,B:] holds f.a = [a`2,a`1]) & (for a be Element of [:A,B:] holds g.a = [a`2,a`1]); now let a be Element of [:A,B:]; f.a = [a`2,a`1] & g.a = [a`2,a`1] by A1; hence f.a = g.a; end; hence thesis by FUNCT_2:113; end; end; theorem for A,B be non empty set holds rng (Inv (A,B)) = [:B,A:] proof let A,B be non empty set; thus rng Inv(A,B) c= [:B,A:]; let x; assume x in [:B,A:]; then reconsider y = x as Element of [:B,A:]; A1: [y`2,y`1] in [:A,B:] & dom Inv (A,B) = [:A,B:] by FUNCT_2:def 1; Inv(A,B).[y`2,y`1] = [[y`2,y`1]`2,[y`2,y`1]`1] by Def6 .= [y`1,[y`2,y`1]`1] by MCART_1:7 .= [y`1,y`2] by MCART_1:7 .= y by MCART_1:23; hence thesis by A1,FUNCT_1:def 5; end; theorem for A,B be non empty set holds Inv (A,B) is one-to-one proof let A,B be non empty set; let x,y; assume A1: x in dom Inv(A,B) & y in dom Inv(A,B) & Inv(A,B).x = Inv(A,B).y; then reconsider x1 = x,y1 = y as Element of [:A,B:] by FUNCT_2:def 1; Inv(A,B).x1 = [x1`2,x1`1] & Inv(A,B).y1 = [y1`2,y1`1] by Def6; then x1`1 =y1`1 & x1`2 = y1`2 by A1,ZFMISC_1:33; hence thesis by DOMAIN_1:12; end; theorem U1,U2 are_similar implies Inv (the carrier of U1,the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:] proof assume U1,U2 are_similar; then [:U1,U2:] = UAStr (# [:the carrier of U1,the carrier of U2:], Opers(U1, U2) #) & [:U2,U1:] = UAStr (# [:the carrier of U2,the carrier of U1:], Opers(U2,U1) #) by Def5; hence thesis; end; theorem Th6: U1,U2 are_similar implies for o1 be operation of U1,o2 be operation of U2,o be operation of [:U1,U2:], n be Nat st o1 = (the charact of U1).n & o2 = (the charact of U2).n & o = (the charact of [:U1,U2:]).n & n in dom the charact of(U1) holds arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] proof assume A1: U1,U2 are_similar; let o1 be operation of U1,o2 be operation of U2,o be operation of [:U1,U2:], n be Nat; assume A2: o1 = (the charact of U1).n & o2 = (the charact of U2).n & o = (the charact of [:U1,U2:]).n & n in dom the charact of(U1); A3: [:U1,U2:] = UAStr (# [:the carrier of U1,the carrier of U2:], Opers(U1,U2) #) by A1,Def5; A4: dom the charact of(U1) = Seg len the charact of(U1) & dom the charact of(U2) = Seg len the charact of(U2) & dom Opers(U1,U2) = Seg len Opers(U1,U2) & dom (signature U1) = Seg len (signature U1) & dom (signature U2) = Seg len (signature U2) by FINSEQ_1:def 3; A5: len the charact of(U1) = len Opers(U1,U2) by A1,Def4; then A6: o = [[:o1,o2:]] by A1,A2,A3,A4,Def4; A7: signature U1 = signature U2 by A1,UNIALG_2:def 2; len signature U1 = len the charact of (U1) & len signature U2 = len the charact of(U2) by UNIALG_1:def 11; then A8: (signature U1).n = arity o1 & (signature U2).n = arity o2 by A2,A4,A7,UNIALG_1:def 11; then A9: dom o = (arity o1)-tuples_on [:the carrier of U1,the carrier of U2:] by A6,A7,Def3; for x be FinSequence of the carrier of [:U1,U2:] st x in dom o holds len x = arity o1 proof let x be FinSequence of the carrier of [:U1,U2:]; assume x in dom o; then x in {s where s is Element of ([:the carrier of U1,the carrier of U2 :])*: len s = arity o1} by A9,FINSEQ_2:def 4; then consider s be Element of ([:the carrier of U1,the carrier of U2:])* such that A10: s = x & len s = arity o1; thus thesis by A10; end; hence thesis by A1,A2,A3,A4,A5,A7,A8,Def4,UNIALG_1:def 10; end; theorem U1,U2 are_similar implies [:U1,U2:],U1 are_similar proof assume A1: U1,U2 are_similar; then [:U1,U2:] = UAStr (# [:the carrier of U1,the carrier of U2:], Opers(U1, U2) #) by Def5; then len the charact of([:U1,U2:]) = len the charact of(U1) by A1,Def4; then A2: len signature ([:U1,U2:]) = len the charact of(U1) by UNIALG_1:def 11 .= len signature(U1) by UNIALG_1:def 11; A3: dom signature(U1) = Seg len signature(U1) & dom signature([:U1,U2:]) = Seg len signature([:U1,U2:]) & dom the charact of(U1) = Seg len the charact of(U1) & dom the charact of(U2) = Seg len the charact of(U2) & dom the charact of([:U1,U2:]) = Seg len the charact of([:U1,U2:]) by FINSEQ_1:def 3; now let n; assume A4: n in Seg len signature(U1); then A5: n in Seg len the charact of(U1) by UNIALG_1:def 11; then n in dom the charact of (U1) by FINSEQ_1:def 3; then reconsider o1 = (the charact of U1).n as operation of U1 by UNIALG_2:6; A6: (signature(U1)).n = arity(o1) by A3,A4,UNIALG_1:def 11; n in dom the charact of([:U1,U2:]) by A2,A3,A4,UNIALG_1:def 11; then reconsider o12 = (the charact of [:U1,U2:]).n as operation of [:U1,U2:] by UNIALG_2:6; A7: (signature([:U1,U2:])).n = arity(o12) by A2,A3,A4,UNIALG_1:def 11; len signature(U1) = len signature(U2) by A1,UNIALG_2:def 2 .= len the charact of(U2) by UNIALG_1:def 11; then reconsider o2 = (the charact of U2).n as operation of U2 by A3,A4,UNIALG_2:6; o1 = (the charact of U1).n & o2 = (the charact of U2).n; hence (signature(U1)).n = (signature([:U1,U2:])).n by A1,A3,A5,A6,A7,Th6; end; then signature(U1) = signature([:U1,U2:]) by A2,FINSEQ_2:10; hence thesis by UNIALG_2:def 2; end; theorem for U1,U2,U3,U4 be Universal_Algebra st U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar holds [:U1,U3:] is SubAlgebra of [:U2,U4:] proof let U1,U2,U3,U4 be Universal_Algebra; assume A1: U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar; then A2: U1,U2 are_similar & U3,U4 are_similar by UNIALG_2:16; then U1,U4 are_similar by A1,UNIALG_2:4; then A3: U1,U3 are_similar by A2,UNIALG_2:4; then A4: [:U1,U3:] = UAStr (# [:the carrier of U1,the carrier of U3:], Opers(U1,U3) #) & [:U2,U4:] = UAStr (# [:the carrier of U2,the carrier of U4:], Opers(U2,U4) #) by A1,Def5; A5: the carrier of U1 is Subset of U2 & the carrier of U3 is Subset of U4 by A1,UNIALG_2:def 8; then A6: [:the carrier of U1,the carrier of U3:] c= [:the carrier of U2,the carrier of U4:] by ZFMISC_1:119; thus the carrier of [:U1,U3:] is Subset of [:U2,U4:] by A4,A5, ZFMISC_1:119; let B be non empty Subset of [:U2,U4:]; assume A7: B = the carrier of [:U1,U3:]; reconsider B1 = the carrier of U1 as non empty Subset of U2 by A1,UNIALG_2:def 8; reconsider B3 = the carrier of U3 as non empty Subset of U4 by A1,UNIALG_2:def 8; A8: B1 is opers_closed & B3 is opers_closed by A1,UNIALG_2:def 8; A9: for o be operation of [:U2,U4:] holds B is_closed_on o proof let o be operation of [:U2,U4:]; let s be FinSequence of B; assume A10: len s = arity o; reconsider s0 = s as Element of ([:the carrier of U1,the carrier of U3:])* by A4,A7,FINSEQ_1:def 11; Operations([:U2,U4:]) = rng the charact of([:U2,U4:]) by UNIALG_2:def 3; then consider n be Nat such that A11: n in dom the charact of([:U2,U4:]) & (the charact of [:U2,U4:]).n = o by FINSEQ_2:11; A12: n in Seg len the charact of ([:U2,U4:]) & (the charact of [:U2,U4:]).n = o by A11,FINSEQ_1:def 3; A13: len the charact of([:U2,U4:]) = len the charact of(U2) by A1,A4,Def4; then A14: n in dom the charact of(U2) by A12,FINSEQ_1:def 3; then reconsider o2 = (the charact of U2).n as operation of U2 by UNIALG_2:6 ; len the charact of(U4) = len the charact of(U2) by A1,UNIALG_2:3; then n in dom the charact of(U4) by A12,A13,FINSEQ_1:def 3; then reconsider o4 = (the charact of U4).n as operation of U4 by UNIALG_2:6 ; o2 = (the charact of U2).n & o4 = (the charact of U4).n; then A15: arity o = arity o2 & arity o = arity o4 & o = [[:o2,o4:]] by A1,A11,A14,Th6; then A16:dom [[:o2,o4:]]=(arity(o2))-tuples_on [:the carrier of U2,the carrier of U4:] by Def3; rng s0 c= [:the carrier of U1,the carrier of U3:] by FINSEQ_1:def 4; then rng s0 c= [:the carrier of U2,the carrier of U4:] by A6,XBOOLE_1:1; then s0 is FinSequence of [:the carrier of U2,the carrier of U4:] by FINSEQ_1:def 4; then reconsider ss = s0 as Element of ([:the carrier of U2,the carrier of U4 :])* by FINSEQ_1:def 11; ss in {w where w is Element of ([:the carrier of U2,the carrier of U4:])* : len w = arity o2 } by A10,A15; then A17: ss in dom [[:o2,o4:]] by A16,FINSEQ_2:def 4; reconsider s1 = pr1 s0 as Element of B1* by FINSEQ_1:def 11; reconsider s3 = pr2 s0 as Element of B3* by FINSEQ_1:def 11; A18: B1 is_closed_on o2 & B3 is_closed_on o4 by A8,UNIALG_2:def 5; len s1 = len s0 & len s3 = len s0 by Def1,Def2; then A19: o2.s1 in B1 & o4.s3 in B3 by A10,A15,A18,UNIALG_2:def 4; o.s = [o2.(pr1 ss),o4.(pr2 ss)] by A15,A17,Def3; hence thesis by A4,A7,A19,ZFMISC_1:106; end; A20: dom the charact of([:U2,U4:]) = dom Opers([:U2,U4:],B) by UNIALG_2:def 7; then len the charact of([:U2,U4:]) = len Opers([:U2,U4:],B) by FINSEQ_3:31; then A21: len the charact of(U2) = len Opers([:U2,U4:],B) by A1,A4,Def4; A22: len the charact of([:U1,U3:]) = len the charact of(U1) by A3,A4,Def4; signature (U1) = signature (U2) by A2,UNIALG_2:def 2; then len the charact of(U1) = len signature(U2) by UNIALG_1:def 11; then A23: len the charact of([:U1,U3:]) = len Opers([:U2,U4:],B) by A21,A22,UNIALG_1:def 11; A24: dom the charact of(U1) = Seg len the charact of(U1) & dom the charact of(U2) = Seg len the charact of(U2) & dom the charact of(U3) = Seg len the charact of(U3) & dom the charact of(U4) = Seg len the charact of(U4) & dom the charact of([:U1,U3:]) = Seg len the charact of([:U1,U3:]) & dom the charact of([:U2,U4:]) = Seg len the charact of([:U2,U4:]) & dom Opers([:U2,U4:],B) = Seg len Opers([:U2,U4:],B) & dom Opers(U2,B1) = Seg len Opers(U2,B1) & dom Opers(U4,B3) = Seg len Opers(U4,B3) by FINSEQ_1:def 3; signature (U4) = signature (U2) by A1,UNIALG_2:def 2; then len the charact of(U4) = len signature(U2) by UNIALG_1:def 11; then A25: len the charact of(U4) = len the charact of(U2) by UNIALG_1:def 11; signature (U1) = signature (U3) by A3,UNIALG_2:def 2; then len the charact of(U1) = len signature(U3) by UNIALG_1:def 11; then A26: len the charact of(U1) = len the charact of(U3) by UNIALG_1:def 11; A27: dom the charact of(U2) = dom Opers(U2,B1) by UNIALG_2:def 7; A28: dom the charact of(U4) = dom Opers(U4,B3) by UNIALG_2:def 7; for n st n in Seg len the charact of([:U1,U3:]) holds (the charact of [:U1,U3:]).n = Opers([:U2,U4:],B).n proof let n; assume A29: n in Seg len the charact of([:U1,U3:]); then reconsider o2 = (the charact of U2).n as operation of U2 by A21,A23,A24,UNIALG_2:6; reconsider o4 = (the charact of U4).n as operation of U4 by A21,A23,A24,A25,A29,UNIALG_2:6; reconsider o24 = (the charact of [:U2,U4:]).n as operation of [:U2,U4:] by A20,A23,A24,A29,UNIALG_2:6; reconsider o1 = (the charact of U1).n as operation of U1 by A22,A24,A29,UNIALG_2:6; reconsider o3 = (the charact of U3).n as operation of U3 by A22,A24,A26,A29,UNIALG_2:6; o2 = (the charact of U2).n & o4 = (the charact of U4).n; then A30: o24 = [[:o2,o4:]] & arity o24 = arity o4 & arity o24 = arity o2 by A1,A21,A23,A24,A29,Th6; A31: Opers(U2,B1).n = o2/. B1 by A21,A23,A24,A27,A29,UNIALG_2:def 7; A32: Opers(U4,B3).n = o4/.B3 by A21,A23,A24,A25,A28,A29,UNIALG_2:def 7; A33: o1 = o2/.B1 by A1,A31,UNIALG_2:def 8; A34: o3 = o4/.B3 by A1,A32,UNIALG_2:def 8; A35: B is_closed_on o24 & B1 is_closed_on o2 & B3 is_closed_on o4 by A8,A9,UNIALG_2:def 5; then A36: arity (o2/.B1) = arity o2 & arity (o4/.B3) = arity o4 by UNIALG_2:8; then A37: dom ([[:o2/.B1,o4/.B3:]]) = (arity o2)-tuples_on B by A4,A7,A30, Def3; A38: dom ([[:o2,o4:]]|((arity o24)-tuples_on B)) = dom ([[:o2,o4:]]) /\ ((arity o2)-tuples_on B) by A30,FUNCT_1:68 .= (arity o2)-tuples_on (the carrier of [:U2,U4:]) /\ ((arity o2)-tuples_on B) by A4,A30,Def3 .= ((arity o2)-tuples_on B) by UNIALG_2:1; A39: now let x; assume A40: x in ((arity o2)-tuples_on B); then x in {s where s is Element of B*: len s = arity o2} by FINSEQ_2:def 4; then consider s be Element of B* such that A41: s = x & len s = arity o2; B c= [:the carrier of U2,the carrier of U4:] & rng s c= B by A4,FINSEQ_1:def 4; then rng s c= [:the carrier of U2,the carrier of U4:] by XBOOLE_1:1; then reconsider s0 = s as FinSequence of [:the carrier of U2,the carrier of U4:] by FINSEQ_1:def 4; A42: dom ([[:o2,o4:]]|((arity o24)-tuples_on B)) c= dom [[:o2,o4:]] by FUNCT_1:76; A43: ([[:o2,o4:]]|((arity o24)-tuples_on B)).x = [[:o2,o4:]].s0 by A38,A40,A41,FUNCT_1: 68 .= [o2.(pr1 s0),o4.(pr2 s0)] by A30,A38,A40,A41,A42,Def3; reconsider s1 = s as FinSequence of [:B1 qua non empty set,B3 qua non empty set:] by A4,A7; reconsider s11 = pr1 s1 as Element of B1* by FINSEQ_1:def 11; reconsider s12 = pr2 s1 as Element of B3* by FINSEQ_1:def 11; len (pr1 s1) = len s1 & len (pr1 s0) = len s0 by Def1; then s11 in {a where a is Element of B1 *: len a = arity o2} by A41; then A44: s11 in (arity o2)-tuples_on B1 by FINSEQ_2:def 4; A45: dom (o2|(arity o2)-tuples_on B1) = dom o2 /\ (arity o2)-tuples_on B1 by FUNCT_1:68 .= ((arity o2)-tuples_on the carrier of U2) /\ (arity o2)-tuples_on B1 by UNIALG_2:2 .= (arity o2)-tuples_on B1 by UNIALG_2:1; len (pr2 s1) = len s1 & len (pr2 s0) = len s0 by Def2; then s12 in {b where b is Element of B3*: len b = arity o4} by A30,A41; then A46: s12 in (arity o4)-tuples_on B3 by FINSEQ_2:def 4; A47: dom (o4|(arity o4)-tuples_on B3) = dom o4 /\ (arity o4)-tuples_on B3 by FUNCT_1:68 .= ((arity o4)-tuples_on the carrier of U4) /\ (arity o4)-tuples_on B3 by UNIALG_2:2 .= (arity o4)-tuples_on B3 by UNIALG_2:1; [[:o2/.B1,o4/.B3:]].x = [(o2/.B1).(pr1 s1),(o4/.B3).(pr2 s1)] by A30,A36,A37,A40,A41,Def3 .= [(o2|((arity o2)-tuples_on B1)).s11,(o4/.B3).(pr2 s1)] by A35,UNIALG_2:def 6 .= [o2.(pr1 s1),(o4/.B3).(pr2 s1)] by A44,A45,FUNCT_1:68 .= [o2.(pr1 s1),(o4|((arity o4)-tuples_on B3)).(pr2 s1)] by A35,UNIALG_2:def 6 .= [o2.(pr1 s1),o4.(pr2 s1)] by A46,A47,FUNCT_1:68; hence [[:o2/.B1,o4/.B3:]].x = ([[:o2,o4:]]|((arity o24)-tuples_on B)).x by A43; end; thus Opers([:U2,U4:],B).n = o24/.B by A23,A24,A29,UNIALG_2:def 7 .= [[:o2,o4:]]|((arity o24)-tuples_on B) by A30,A35,UNIALG_2:def 6 .= [[:o2/.B1,o4/.B3:]] by A37,A38,A39,FUNCT_1:9 .= (the charact of [:U1,U3:]).n by A3,A4,A24,A29,A33,A34,Def4; end; hence thesis by A9,A23,FINSEQ_2:10,UNIALG_2:def 5; end; begin :: :: Trivial Algebra :: definition let k be natural number; func TrivialOp(k) -> PartFunc of {{}}*,{{}} means :Def7: dom it = { k |-> {}} & rng it = {{}}; existence proof consider f be Function such that A1: dom f = {k |-> {}} & rng f = {{}} by FUNCT_1:15; dom f c= {{}}* proof let x; assume A2: x in dom f; reconsider a = {} as Element of {{}} by TARSKI:def 1; x = k |-> a by A1,A2,TARSKI:def 1; then x is FinSequence of {{}} by FINSEQ_2:77; hence thesis by FINSEQ_1:def 11; end; then reconsider f as PartFunc of {{}}*,{{}} by A1,RELSET_1:11; take f; thus thesis by A1; end; uniqueness by FUNCT_1:17; end; definition let k be natural number; cluster TrivialOp k -> homogeneous quasi_total non empty; coherence proof set f = TrivialOp k; A1: dom f = {k |-> {}} & rng f = {{}} by Def7; thus f is homogeneous proof let x,y be FinSequence of {{}}; assume x in dom f & y in dom f; then x = k |-> {} & y = k |-> {} by A1,TARSKI:def 1; hence len x = len y; end; now let x,y be FinSequence of {{}}; assume A2: len x = len y & x in dom f ; then A3: x = k |-> {} by A1,TARSKI:def 1; then A4: len x = k by FINSEQ_2:69; now let n; assume A5: n in Seg len x; then A6: x.n = {} by A3,A4,FINSEQ_2:70; n in dom y by A2,A5,FINSEQ_1:def 3; then y.n in {{}} by FINSEQ_2:13; hence x.n = y.n by A6,TARSKI:def 1; end; hence y in dom f by A2,FINSEQ_2:10; end; hence f is quasi_total non empty by A1,UNIALG_1:1,def 2; end; end; theorem for k being natural number holds arity TrivialOp(k) = k proof let k be natural number; A1:k is Nat by ORDINAL2:def 21; now let x be FinSequence of {{}}; assume x in dom TrivialOp(k); then x in {k |-> {}} by Def7; then x = k |-> {} by TARSKI:def 1; hence len x = k by FINSEQ_2:69; end; hence thesis by A1,UNIALG_1:def 10; end; definition let f be FinSequence of NAT; func TrivialOps(f) -> PFuncFinSequence of {{}} means :Def8: len it = len f & for n st n in dom it for m st m = f.n holds it.n=TrivialOp(m); existence proof defpred P[set,set] means for m st m = f.$1 holds $2 = TrivialOp(m); A1: for k st k in Seg len f ex x being Element of PFuncs({{}}* ,{{}}) st P[k,x] proof let k; assume k in Seg len f; then k in dom f by FINSEQ_1:def 3; then reconsider k1 = f.k as Nat by FINSEQ_2:13; reconsider A = TrivialOp(k1) as Element of PFuncs({{}}*,{{} }) by PARTFUN1:119; take A; let m; assume m = f.k; hence thesis; end; consider p being FinSequence of PFuncs({{}}*,{{}}) such that A2: dom p = Seg len f & for k st k in Seg len f holds P[k,p.k] from SeqDEx(A1); reconsider p as PFuncFinSequence of {{}}; take p; thus len p = len f by A2,FINSEQ_1:def 3; let n; assume n in dom p; hence thesis by A2; end; uniqueness proof let x,y be PFuncFinSequence of {{}}; assume A3: (len x=len f & for n st n in dom x for m st m = f.n holds x.n=TrivialOp(m)) & (len y=len f & for n st n in dom y for m st m = f.n holds y.n=TrivialOp(m)); now let n; assume n in Seg len f; then A4: n in dom f & n in dom x & n in dom y by A3,FINSEQ_1:def 3; then reconsider m = f.n as Nat by FINSEQ_2:13; x.n=TrivialOp(m) & y.n=TrivialOp(m) by A3,A4; hence x.n = y.n; end; hence thesis by A3,FINSEQ_2:10; end; end; theorem Th10: for f be FinSequence of NAT holds TrivialOps(f) is homogeneous quasi_total non-empty proof let f be FinSequence of NAT; A1: for n be Nat,h be PartFunc of {{}}*,{{}} st n in dom TrivialOps(f) & h = (TrivialOps(f)).n holds h is homogeneous proof let n be Nat,h be PartFunc of {{}}*,{{}}; assume A2: n in dom TrivialOps(f) & (TrivialOps(f)).n = h; dom TrivialOps(f) = Seg len TrivialOps(f) by FINSEQ_1:def 3 .= Seg len f by Def8 .= dom f by FINSEQ_1:def 3; then reconsider m = f.n as Nat by A2,FINSEQ_2:13; (TrivialOps(f)).n = TrivialOp(m) by A2,Def8; hence h is homogeneous by A2; end; A3: for n be Nat,h be PartFunc of {{}}*,{{}} st n in dom TrivialOps(f) & h = (TrivialOps(f)).n holds h is quasi_total proof let n be Nat,h be PartFunc of {{}}*,{{}}; assume A4: n in dom TrivialOps(f) & (TrivialOps(f)).n = h; dom TrivialOps(f) = Seg len TrivialOps(f) by FINSEQ_1:def 3 .= Seg len f by Def8 .= dom f by FINSEQ_1:def 3; then reconsider m = f.n as Nat by A4,FINSEQ_2:13; (TrivialOps(f)).n = TrivialOp(m) by A4,Def8; hence h is quasi_total by A4; end; for n be set st n in dom TrivialOps(f) holds (TrivialOps(f)).n is non empty proof let n be set; assume A5: n in dom TrivialOps(f); then reconsider k = n as Nat; dom TrivialOps(f) = Seg len TrivialOps(f) by FINSEQ_1:def 3 .= Seg len f by Def8 .= dom f by FINSEQ_1:def 3; then reconsider m = f.k as Nat by A5,FINSEQ_2:13; (TrivialOps(f)).k = TrivialOp(m) by A5,Def8; hence (TrivialOps(f)).n is non empty; end; hence thesis by A1,A3,UNIALG_1:def 4,def 5,def 6; end; theorem Th11: for f be FinSequence of NAT st f <> {} holds UAStr (#{{}},TrivialOps(f)#) is strict Universal_Algebra proof let f be FinSequence of NAT; assume A1: f <> {}; set U0 = UAStr (#{{}},TrivialOps(f)#); A2: the charact of U0 is homogeneous quasi_total non-empty by Th10; len (the charact of U0) = len f by Def8; then len (the charact of U0) <> 0 by A1,FINSEQ_1:25; then the charact of U0 <> {} by FINSEQ_1:25; hence thesis by A2,UNIALG_1:def 7,def 8,def 9; end; definition let D be non empty set; cluster non empty FinSequence of D; existence proof consider d being Element of D; take <*d*>; <*d*> = { [1,d] } by FINSEQ_1:52; hence thesis; end; cluster non empty Element of D*; existence proof consider d being Element of D; reconsider e = <*d*> as Element of D* by FINSEQ_1:def 11; take e; e = { [1,d] } by FINSEQ_1:52; hence thesis; end; end; definition let f be non empty FinSequence of NAT; func Trivial_Algebra(f) -> strict Universal_Algebra equals UAStr (#{{}},TrivialOps(f)#); coherence by Th11; end; begin :: :: Product of Universal Algebras :: definition let IT be Function; attr IT is Univ_Alg-yielding means :Def10: for x st x in dom IT holds IT.x is Universal_Algebra; end; definition let IT be Function; attr IT is 1-sorted-yielding means :Def11: for x st x in dom IT holds IT.x is 1-sorted; end; definition cluster Univ_Alg-yielding Function; existence proof reconsider f = {} as Function; take f; let x; thus thesis by RELAT_1:60; end; end; definition cluster Univ_Alg-yielding -> 1-sorted-yielding Function; coherence proof let F be Function; assume F is Univ_Alg-yielding; then for x st x in dom F holds F.x is 1-sorted by Def10; hence F is 1-sorted-yielding by Def11; end; end; definition let I be set; cluster 1-sorted-yielding ManySortedSet of I; existence proof consider A be 1-sorted; set f = I --> A; A1: dom f = I by FUNCOP_1:19; then reconsider f as ManySortedSet of I by PBOOLE:def 3; take f; for i be set st i in dom f holds f.i is 1-sorted by A1,FUNCOP_1:13; hence thesis by Def11; end; end; definition let IT be Function; attr IT is equal-signature means :Def12: for x,y st x in dom IT & y in dom IT holds for U1,U2 st U1 = IT.x & U2 = IT.y holds signature U1 = signature U2; end; definition let J be non empty set; cluster equal-signature Univ_Alg-yielding ManySortedSet of J; existence proof consider U1; set f = J --> U1; A1: dom f = J by FUNCOP_1:19; then reconsider f as ManySortedSet of J by PBOOLE:def 3; take f; for x,y st x in dom f & y in dom f holds for U1,U2 st U1 = f.x & U2 = f.y holds signature U1 = signature U2 proof let x,y; assume x in dom f & y in dom f; then A2: f.x = U1 & f.y = U1 by A1,FUNCOP_1:13; let U2,U3; assume U2 = f.x & U3 = f.y; hence thesis by A2; end; hence f is equal-signature by Def12; for x st x in dom f holds f.x is Universal_Algebra by A1,FUNCOP_1:13; hence f is Univ_Alg-yielding by Def10; end; end; definition let J be non empty set, A be 1-sorted-yielding ManySortedSet of J, j be Element of J; redefine func A.j -> 1-sorted; coherence proof dom A = J by PBOOLE:def 3; hence thesis by Def11; end; end; definition let J be non empty set, A be Univ_Alg-yielding ManySortedSet of J, j be Element of J; redefine func A.j -> Universal_Algebra; coherence proof dom A = J by PBOOLE:def 3; hence thesis by Def10; end; end; definition let J be set, A be 1-sorted-yielding ManySortedSet of J; func Carrier A -> ManySortedSet of J means :Def13: for j be set st j in J ex R being 1-sorted st R = A.j & it.j = the carrier of R; existence proof defpred P[set,set] means ex R being 1-sorted st R = A.$1 & $2 = the carrier of R; A1: for i be set st i in J ex j be set st P[i,j] proof let i be set; assume A2: i in J; then reconsider J as non empty set; reconsider B = A as 1-sorted-yielding ManySortedSet of J; reconsider i' = i as Element of J by A2; take j = the carrier of B.i', R = B.i'; thus R = A.i & j = the carrier of R; end; consider M being Function such that A3: dom M = J and A4: for i being set st i in J holds P[i,M.i] from NonUniqFuncEx(A1); reconsider M as ManySortedSet of J by A3,PBOOLE:def 3; take M; thus thesis by A4; end; uniqueness proof let X,Y be ManySortedSet of J; assume that A5: for j be set st j in J ex R being 1-sorted st R = A.j & X.j = the carrier of R and A6: for j be set st j in J ex R being 1-sorted st R = A.j & Y.j = the carrier of R; for i be set st i in J holds X.i = Y.i proof let i be set; assume i in J; then (ex R being 1-sorted st R = A.i & X.i = the carrier of R) & ex R being 1-sorted st R = A.i & Y.i = the carrier of R by A5,A6; hence thesis; end; hence thesis by PBOOLE:3; end; end; definition let J be non empty set, A be Univ_Alg-yielding ManySortedSet of J; cluster Carrier A -> non-empty; coherence proof let i be set; assume A1: i in J; then consider R being 1-sorted such that A2: R = A.i and A3: (Carrier A).i = the carrier of R by Def13; dom A = J by PBOOLE:def 3; then R is Universal_Algebra by A1,A2,Def10; hence thesis by A3,STRUCT_0:def 1; end; end; definition let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J; func ComSign A -> FinSequence of NAT means :Def14: for j be Element of J holds it = signature (A.j); existence proof consider j be Element of J; A1:dom A = J by PBOOLE:def 3; reconsider U0 = A.j as Universal_Algebra; take signature U0; let j1 be Element of J; thus thesis by A1,Def12; end; uniqueness proof let X,Y be FinSequence of NAT; assume that A2: for j be Element of J holds X = signature (A.j) and A3: for j be Element of J holds Y = signature (A.j); consider j be Element of J; reconsider U0 = A.j as Universal_Algebra; X = signature U0 & Y = signature U0 by A2,A3; hence thesis; end; end; definition let IT be Function; attr IT is Function-yielding means :Def15: for x st x in dom IT holds IT.x is Function; end; definition cluster Function-yielding Function; existence proof consider f being Function,I be set; A1: dom (I --> f) = I by FUNCOP_1:19; take F = I --> f; let x; assume x in dom F; hence thesis by A1,FUNCOP_1:13; end; end; definition let I be set; cluster Function-yielding ManySortedSet of I; existence proof consider f being Function; A1: dom (I --> f) = I by FUNCOP_1:19; then reconsider F = I --> f as ManySortedSet of I by PBOOLE:def 3; take F; let x; assume x in dom F; hence thesis by A1,FUNCOP_1:13; end; end; definition let I be set; mode ManySortedFunction of I is Function-yielding ManySortedSet of I; end; definition let B be Function-yielding Function, j be set; cluster B.j -> Function-like Relation-like; coherence proof per cases; suppose j in dom B; hence thesis by Def15; suppose not j in dom B; hence thesis by FUNCT_1:def 4; end; end; definition let J be non empty set, B be non-empty ManySortedSet of J, j be Element of J; cluster B.j -> non empty; coherence by PBOOLE:def 16; end; definition let F be Function-yielding Function, f be Function; cluster F * f -> Function-yielding; coherence proof thus F * f is Function-yielding proof let x be set; assume x in dom (F*f); then (F*f).x = F.(f.x) by FUNCT_1:22; hence (F*f).x is Function; end; end; end; definition let J be non empty set, B be non-empty ManySortedSet of J; cluster product B -> non empty; coherence; end; definition let J be non empty set, B be non-empty ManySortedSet of J; mode ManySortedOperation of B -> ManySortedFunction of J means :Def16: for j be Element of J holds it.j is homogeneous quasi_total non empty PartFunc of (B.j)*,B.j; existence proof defpred P[set,set] means $2 in B.$1; A1: for x st x in J ex y st P[x,y] proof let x; assume x in J; then B.x <> {} by PBOOLE:def 16; hence thesis by XBOOLE_0:def 1; end; consider f be Function such that A2: dom f = J & for x st x in J holds P[x,f.x] from NonUniqFuncEx(A1); deffunc G(set) = {<*>(B.$1)} --> f.$1; consider F being Function such that A3: dom F = J & for x st x in J holds F.x = G(x) from Lambda; reconsider F as ManySortedSet of J by A3,PBOOLE:def 3; for x st x in dom F holds F.x is Function proof let x; assume x in dom F; then F.x = {<*>(B.x)} --> f.x by A3; hence thesis; end; then reconsider F as ManySortedFunction of J by Def15; take F; let j be Element of J; reconsider b = f.j as Element of (B.j) by A2; F.j = {<*>(B.j)} --> b by A3; hence thesis by UNIALG_1:2; end; end; definition let J be non empty set, B be non-empty ManySortedSet of J, O be ManySortedOperation of B, j be Element of J; redefine func O.j ->homogeneous quasi_total non empty PartFunc of (B.j)*,B.j; coherence by Def16; end; definition let IT be Function; attr IT is equal-arity means :Def17: for x,y be set st x in dom IT & y in dom IT for f,g be Function st IT.x = f & IT.y = g holds for n,m be Nat for X,Y be non empty set st dom f = n-tuples_on X & dom g = m-tuples_on Y holds for o1 be homogeneous quasi_total non empty PartFunc of X*,X, o2 be homogeneous quasi_total non empty PartFunc of Y*,Y st f = o1 & g = o2 holds arity o1 = arity o2; end; definition let J be non empty set, B be non-empty ManySortedSet of J; cluster equal-arity ManySortedOperation of B; existence proof defpred P[set,set] means $2 in B.$1; A1: for x st x in J ex y st P[x,y] proof let x; assume x in J; then B.x <> {} by PBOOLE:def 16; hence thesis by XBOOLE_0:def 1; end; consider f be Function such that A2: dom f = J & for x st x in J holds P[x,f.x] from NonUniqFuncEx(A1); deffunc G(set) = {<*>(B.$1)} --> f.$1; consider F being Function such that A3: dom F = J & for x st x in J holds F.x = G(x) from Lambda; reconsider F as ManySortedSet of J by A3,PBOOLE:def 3; for x st x in dom F holds F.x is Function proof let x; assume x in dom F; then F.x = {<*>(B.x)} --> f.x by A3; hence thesis; end; then reconsider F as ManySortedFunction of J by Def15; now let j be Element of J; reconsider b = f.j as Element of (B.j) by A2; F.j = {<*>(B.j)} --> b by A3; hence F.j is homogeneous quasi_total non empty PartFunc of (B.j)*,B.j by UNIALG_1:2; end; then reconsider F as ManySortedOperation of B by Def16; take F; for x,y be set st x in dom F & y in dom F for f,g be Function st F.x = f & F.y = g holds for n,m be Nat for X,Y be non empty set st dom f = n-tuples_on X & dom g = m-tuples_on Y holds for o1 be homogeneous quasi_total non empty PartFunc of X*,X, o2 be homogeneous quasi_total non empty PartFunc of Y*,Y st f = o1 & g = o2 holds arity o1 = arity o2 proof let x,y; assume A4: x in dom F & y in dom F; then reconsider x1 = x, y1 = y as Element of J by A3; let g,h be Function; assume A5: F.x = g & F.y = h; let n,m be Nat; let X,Y be non empty set; assume dom g = n-tuples_on X & dom h = m-tuples_on Y; let o1 be homogeneous quasi_total non empty PartFunc of X*,X, o2 be homogeneous quasi_total non empty PartFunc of Y*,Y; assume g = o1 & h = o2; then A6: o1 = {<*>(B.x)} --> f.x & o2 = {<*>(B.y)} --> f.y by A3,A4,A5; reconsider fx = f.x1 as Element of B.x1 by A2; reconsider fy = f.y1 as Element of B.y1 by A2; reconsider o1x = {<*>(B.x1)} --> fx as homogeneous quasi_total non empty PartFunc of (B.x1)*,B.x1 by UNIALG_1:2; reconsider o2y = {<*>(B.y1)} --> fy as homogeneous quasi_total non empty PartFunc of (B.y1)*,B.y1 by UNIALG_1:2; A7: dom o1x = {{}(B.x1)} & dom o2y = {{}(B.y1)} by FUNCOP_1:19; consider p1 be set such that A8: p1 in dom o1 by XBOOLE_0:def 1; dom o1 c= X* by RELSET_1:12; then reconsider p1 as Element of X* by A8; p1 = <*>(B.x1) by A6,A7,A8,TARSKI:def 1; then len p1 = 0 by FINSEQ_1:32; then A9: arity o1 = 0 by A8,UNIALG_1:def 10; consider p2 be set such that A10: p2 in dom o2 by XBOOLE_0:def 1; dom o2 c= Y* by RELSET_1:12; then reconsider p2 as Element of Y* by A10; p2 = <*>(B.y1) by A6,A7,A10,TARSKI:def 1; then len p2 = 0 by FINSEQ_1:32; hence thesis by A9,A10,UNIALG_1:def 10; end; hence F is equal-arity by Def17; end; end; theorem Th12: for J be non empty set, B be non-empty ManySortedSet of J, O be ManySortedOperation of B holds O is equal-arity iff for i,j be Element of J holds arity (O.i) = arity (O.j) proof let J be non empty set, B be non-empty ManySortedSet of J, O be ManySortedOperation of B; thus O is equal-arity implies for i,j be Element of J holds arity (O.i) = arity (O.j) proof assume A1: O is equal-arity; let i,j be Element of J; A2: dom O = J by PBOOLE:def 3; dom (O.i) = arity(O.i)-tuples_on (B.i) & dom (O.j) = arity(O.j)-tuples_on (B.j) by UNIALG_2:2; hence thesis by A1,A2,Def17; end; assume A3: for i,j be Element of J holds arity (O.i) = arity (O.j); let x,y be set; assume A4: x in dom O & y in dom O; let f,g be Function; assume A5: O.x = f & O.y = g; let n,m be Nat; let X,Y be non empty set; assume A6: dom f = n-tuples_on X & dom g = m-tuples_on Y; let o1 be homogeneous quasi_total non empty PartFunc of X*,X, o2 be homogeneous quasi_total non empty PartFunc of Y*,Y; assume A7: f = o1 & g = o2; reconsider x1 = x, y1 = y as Element of J by A4,PBOOLE:def 3; arity (O.x1) = arity (O.y1) by A3; then dom f = (arity (O.x1))-tuples_on (B.x1) & dom g = (arity (O.x1))-tuples_on (B.y1) by A5,UNIALG_2:2; then A8: n = arity (O.x1) & m = arity (O.x1) by A6,Th1; consider p be Element of n-tuples_on X; A9: arity o1 = len p by A6,A7,UNIALG_1:def 10 .= n by FINSEQ_2:109; consider q be Element of m-tuples_on Y; arity o2 = len q by A6,A7,UNIALG_1:def 10 .= m by FINSEQ_2:109; hence arity o1 = arity o2 by A8,A9; end; definition let F be Function-yielding Function, f be Function; func F..f -> Function means :Def18: dom it = dom F & for x be set st x in dom F holds it.x = (F.x).(f.x); existence proof defpred P[set,set] means $2 = (F.$1).(f.$1); set I = dom F; A1: for i be set st i in I ex y be set st P[i,y]; consider F be Function such that A2: dom F = I & for i be set st i in I holds P[i,F.i] from NonUniqFuncEx(A1); take F; thus thesis by A2; end; uniqueness proof let m,n be Function; assume that A3: dom m = dom F & for x be set st x in dom F holds m.x = (F.x).(f.x) and A4: dom n = dom F & for x be set st x in dom F holds n.x = (F.x).(f.x); for x be set st x in dom m holds m.x = n.x proof let x; assume A5: x in dom m; consider g be set such that A6: g = F.x; reconsider g as Function by A6; m.x = g.(f.x) & n.x = g.(f.x) by A3,A4,A5,A6; hence thesis; end; hence thesis by A3,A4,FUNCT_1:9; end; end; definition let I be set, f be ManySortedFunction of I, x be ManySortedSet of I; redefine func f..x -> ManySortedSet of I means :Def19: for i be set st i in I holds for g be Function st g = f.i holds it.i = g.(x.i); coherence proof dom(f..x) = dom f by Def18 .= I by PBOOLE:def 3; hence thesis by PBOOLE:def 3; end; compatibility proof let M be ManySortedSet of I; hereby assume M = f..x; then A1: dom M = dom f & for i be set st i in dom f holds M.i = (f.i).(x.i) by Def18; dom M = I by PBOOLE:def 3; hence for i be set st i in I holds for g be Function st g = f.i holds M.i = g.(x.i) by A1; end; assume A2: for i be set st i in I holds for g be Function st g = f.i holds M.i = g.(x.i); A3: dom M = I by PBOOLE:def 3; A4: dom f = I by PBOOLE:def 3; then for i be set st i in dom f holds M.i = (f.i).(x.i) by A2; hence M = f..x by A3,A4,Def18; end; end; definition let J be non empty set, B be non-empty ManySortedSet of J, p be FinSequence of product B; redefine func uncurry p -> ManySortedSet of [:dom p, J:]; coherence proof now consider j be Element of J; dom B = J by PBOOLE:def 3; then B.j in rng B by FUNCT_1:def 5; then B.j c= union rng B by ZFMISC_1:92; then reconsider S = union rng B as non empty set by XBOOLE_1:3; rng p c= Funcs(J,S) proof let x; assume A1: x in rng p; rng p c= product B by FINSEQ_1:def 4; then consider f be Function such that A2: x = f & dom f = dom B & for y st y in dom B holds f.y in B.y by A1,CARD_3:def 5; A3: dom B = J by PBOOLE:def 3; rng f c= S proof let z; assume z in rng f; then consider y such that A4: y in dom f & z = f.y by FUNCT_1:def 5; A5: z in B.y by A2,A4; B.y in rng B by A2,A4,FUNCT_1:def 5; then B.y c= union rng B by ZFMISC_1:92; hence thesis by A5; end; hence thesis by A2,A3,FUNCT_2:def 2; end; then dom (uncurry p) = [:dom p,J:] by FUNCT_5:33; hence thesis by PBOOLE:def 3; end; hence thesis; end; end; definition let I,J be set, X be ManySortedSet of [:I,J:]; redefine func ~X -> ManySortedSet of [:J,I:]; coherence proof dom X = [:I,J:] by PBOOLE:def 3; then dom ~X = [:J,I:] by FUNCT_4:47; hence thesis by PBOOLE:def 3; end; end; definition let X be set, Y be non empty set, f be ManySortedSet of [:X,Y:]; redefine func curry f -> ManySortedSet of X; coherence proof set a = curry f; A1: dom f = [:X,Y:] by PBOOLE:def 3; dom a = proj1 dom f by FUNCT_5:def 3; then dom a = X by A1,FUNCT_5:11; hence thesis by PBOOLE:def 3; end; end; definition let J be non empty set, B be non-empty ManySortedSet of J, O be equal-arity ManySortedOperation of B; func ComAr(O) -> Nat means :Def20: for j be Element of J holds it = arity (O.j); existence proof consider i be Element of J; take arity (O.i); let j be Element of J; thus thesis by Th12; end; uniqueness proof let n,m be Nat; assume A1: (for j be Element of J holds n = arity (O.j)) & for j be Element of J holds m = arity (O.j); consider j be Element of J; n = arity (O.j) & m = arity (O.j) by A1; hence thesis; end; end; definition let I be set, A be ManySortedSet of I; func EmptySeq(A) -> ManySortedSet of I means :Def21: for i be set st i in I holds it.i = {}(A.i); existence proof deffunc F(set) = {}(A.$1); consider f being Function such that A1: dom f = I & for x st x in I holds f.x = F(x) from Lambda; reconsider f as ManySortedSet of I by A1,PBOOLE:def 3; take f; thus thesis by A1; end; uniqueness proof let X,Y be ManySortedSet of I; assume A2: (for i be set st i in I holds X.i = {}(A.i)) & for i be set st i in I holds Y.i = {}(A.i); for i be set st i in I holds X.i = Y.i proof let i be set; assume i in I; then X.i = {}(A.i) & Y.i = {}(A.i) by A2; hence thesis; end; hence thesis by PBOOLE:3; end; end; definition let J be non empty set, B be non-empty ManySortedSet of J, O be equal-arity ManySortedOperation of B; func [[: O :]] -> homogeneous quasi_total non empty PartFunc of (product B)*,(product B) means dom it = (ComAr O)-tuples_on (product B) & for p being Element of (product B)* st p in dom it holds ( dom p = {} implies it.p = O..(EmptySeq B) ) & ( dom p <> {} implies for Z be non empty set, w be ManySortedSet of [:J,Z:] st Z = dom p & w = ~uncurry p holds it.p = O..(curry w)); existence proof set pr = product B, ca = ComAr O, ct = ca-tuples_on pr; defpred P[set,set] means for p being Element of pr* st p = $1 holds ( dom p = {} implies $2 = O..(EmptySeq B) ) & ( dom p <> {} implies for Z be non empty set, w be ManySortedSet of [:J,Z:] st Z = dom p & w = ~uncurry p holds $2 = O..(curry w)); set aa = {q where q is Element of pr* : len q = ca}; A1: ct = aa by FINSEQ_2:def 4; A2: for x st x in ct ex y st y in pr & P[x,y] proof let x; assume x in ct; then consider w be Element of pr* such that A3: x = w & len w = ca by A1; now per cases; case A4: dom w = {}; take y = O..(EmptySeq B); A5: dom (O..(EmptySeq B)) = J by PBOOLE:def 3 .= dom B by PBOOLE:def 3; for z st z in dom B holds (O..(EmptySeq B)).z in B.z proof let z; assume z in dom B; then reconsider j = z as Element of J by PBOOLE:def 3; A6: (O..(EmptySeq B)).z = (O.j).((EmptySeq B).j) by Def19 .= (O.j).({}(B.j)) by Def21; w = {} by A4,FINSEQ_1:26; then len w = 0 by FINSEQ_1:25; then arity (O.j) = 0 by A3,Def20; then dom (O.j) = 0-tuples_on (B.j) by UNIALG_2:2 .= {<*>(B.j)} by FINSEQ_2:112; then {}(B.j) in dom (O.j) by TARSKI:def 1; then (O.j).({}(B.j)) in rng (O.j) & rng (O.j) c= B.j by FUNCT_1:def 5,RELSET_1:12; hence thesis by A6; end; hence y in pr by A5,CARD_3:def 5; let p be Element of pr*; assume p = x; hence (dom p = {} implies y = O..(EmptySeq B)) & (dom p <> {} implies for Z be non empty set, w be ManySortedSet of [:J,Z:] st Z = dom p & w = ~uncurry p holds y = O..(curry w)) by A3,A4; case dom w <> {}; then reconsider Z = dom w as non empty set; reconsider p = ~uncurry w as ManySortedSet of [:J,Z:]; take y = O..(curry p); A7: dom (O..(curry p)) = J by PBOOLE:def 3 .= dom B by PBOOLE:def 3; for z st z in dom B holds (O..(curry p)).z in B.z proof let z; assume z in dom B; then reconsider j = z as Element of J by PBOOLE:def 3; A8: (O..(curry p)).z = (O.j).((curry p).j) by Def19; A9: dom p = [:J,Z:] by PBOOLE:def 3; then A10: proj1 dom p = J & proj2 dom p = Z by FUNCT_5:11; then consider g be Function such that A11: (curry p).j = g & dom g = proj2 (dom p /\ [:{j},proj2 dom p:]) & for y st y in dom g holds g.y = p.[j,y] by FUNCT_5:def 3; A12: dom g = proj2 [:J /\ {j},Z /\ Z:] by A9,A10,A11,ZFMISC_1:123 .= proj2 [:{j},Z:] by ZFMISC_1:52 .= dom w by FUNCT_5:11 .= Seg len w by FINSEQ_1:def 3; then reconsider g as FinSequence by FINSEQ_1:def 2; rng g c= B.j proof let y; assume y in rng g; then consider x such that A13: x in dom g & g.x = y by FUNCT_1:def 5; A14: y = (~uncurry w).[j,x] by A11,A13; A15: dom (uncurry w) = [:dom w,J:] by PBOOLE:def 3; dom g = dom w by A12,FINSEQ_1:def 3; then A16: [x,j] in dom (uncurry w) by A13,A15,ZFMISC_1:106; then A17: y = (uncurry w).[x,j] by A14,FUNCT_4:def 2; consider a be set,f be Function, b be set such that A18: [x,j] = [a,b] & a in dom w & f = w.a & b in dom f by A16,FUNCT_5:def 4; A19: x = a & j = b by A18,ZFMISC_1:33; A20: rng w c= pr by FINSEQ_1:def 4; w.a in rng w by A18,FUNCT_1:def 5; then A21: dom f = dom B & for e be set st e in dom B holds f.e in B.e by A18,A20,CARD_3:18; [a,b]`1 = a & [a,b]`2 = j by A18,MCART_1:7; then y = f.j by A16,A17,A18,FUNCT_5:def 4; hence y in B.j by A18,A19,A21; end; then reconsider g as FinSequence of B.j by FINSEQ_1:def 4; reconsider g as Element of (B.j)* by FINSEQ_1:def 11; A22: len g = len w by A12,FINSEQ_1:def 3; arity (O.j) = ca by Def20; then dom (O.j) = ca-tuples_on (B.j) by UNIALG_2:2 .= {s where s is Element of (B.j)* : len s = ca} by FINSEQ_2:def 4; then g in dom (O.j) by A3,A22; then (O.j).g in rng (O.j) & rng (O.j) c= B.j by FUNCT_1:def 5,RELSET_1:12; hence thesis by A8,A11; end; hence y in pr by A7,CARD_3:def 5; let l be Element of pr*; assume l = x; hence (dom l = {} implies y = O..(EmptySeq B)) & (dom l <> {} implies for Z be non empty set, w be ManySortedSet of [:J,Z:] st Z = dom l & w = ~uncurry l holds y = O..(curry w)) by A3; end; hence thesis; end; consider f being Function such that A23: dom f = ct & rng f c= pr & for x st x in ct holds P[x,f.x] from NonUniqBoundFuncEx(A2); ct in {n-tuples_on pr : not contradiction}; then ct c= union {m-tuples_on pr : not contradiction} by ZFMISC_1:92; then dom f c= pr* by A23,FINSEQ_2:128; then reconsider f as PartFunc of pr*,pr by A23,RELSET_1:11; A24: f is homogeneous proof let x,y be FinSequence of pr; assume A25:x in dom f & y in dom f; reconsider x1 = x, y1 = y as Element of pr* by FINSEQ_1:def 11; (ex w be Element of pr* st x1 = w & len w = ca) & ex w be Element of pr* st y1 = w & len w = ca by A1,A23,A25; hence thesis; end; f is quasi_total proof let x,y be FinSequence of pr; assume A26:len x = len y & x in dom f; reconsider x1 = x, y1 = y as Element of pr* by FINSEQ_1:def 11; ex w be Element of pr* st x1 = w & len w = ca by A1,A23,A26; then y1 in aa by A26; hence thesis by A23,FINSEQ_2:def 4; end; then reconsider f as homogeneous quasi_total non empty PartFunc of pr*,pr by A23,A24,UNIALG_1:1; take f; thus dom f = ct by A23; let p be Element of pr*; assume p in dom f; hence thesis by A23; end; uniqueness proof set pr = product B, ca = ComAr O; let f,g be homogeneous quasi_total non empty PartFunc of pr*,pr; assume that A27: dom f = ca-tuples_on pr & for p being Element of pr* st p in dom f holds (dom p = {} implies f.p = O..(EmptySeq B) ) & (dom p <> {} implies for Z be non empty set, w be ManySortedSet of [:J,Z:] st Z = dom p & w = ~uncurry p holds f.p = O..(curry w)) and A28: dom g = ca-tuples_on pr & for p being Element of pr* st p in dom g holds (dom p = {} implies g.p = O..(EmptySeq B) ) & (dom p <> {} implies for Z be non empty set, w be ManySortedSet of [:J,Z:] st Z = dom p & w = ~uncurry p holds g.p = O..(curry w)); for x st x in ca-tuples_on pr holds f.x = g.x proof let x; assume A29: x in ca-tuples_on pr; then x in { s where s is Element of pr* : len s = ca} by FINSEQ_2:def 4; then consider s be Element of pr* such that A30: x = s & len s = ca; now per cases; case dom s = {}; then f.s = O..(EmptySeq B) & g.s = O..(EmptySeq B) by A27,A28,A29,A30 ; hence thesis by A30; case dom s <> {}; then reconsider Z = dom s as non empty set; reconsider w = ~uncurry s as ManySortedSet of [:J,Z:]; f.s = O..(curry w) & g.s = O..(curry w) by A27,A28,A29,A30; hence thesis by A30; end; hence thesis; end; hence thesis by A27,A28,FUNCT_1:9; end; end; definition let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J, n be natural number; assume A1: n in dom (ComSign A); func ProdOp(A,n) -> equal-arity ManySortedOperation of (Carrier A) means for j be Element of J holds for o be operation of A.j st (the charact of A.j).n = o holds it.j = o; existence proof defpred P[set,set] means for j be Element of J st $1 = j holds for o be operation of A.j st (the charact of A.j).n = o holds $2 = o; A2: for x st x in J ex y st P[x,y] proof let x; assume x in J; then reconsider x1 = x as Element of J; n in dom (signature (A.x1)) by A1,Def14; then n in Seg len (signature (A.x1)) by FINSEQ_1:def 3; then n in Seg len (the charact of(A.x1)) by UNIALG_1:def 11; then n in dom (the charact of(A.x1)) by FINSEQ_1:def 3; then reconsider o = (the charact of A.x1).n as operation of A.x1 by UNIALG_2:6; take o; let j be Element of J; assume A3: x = j; let o1 be operation of A.j; assume (the charact of A.j).n = o1; hence thesis by A3; end; consider f be Function such that A4: dom f = J & for x st x in J holds P[x,f.x] from NonUniqFuncEx(A2); reconsider f as ManySortedSet of J by A4,PBOOLE:def 3; for x st x in dom f holds f.x is Function proof let x; assume x in dom f; then reconsider x1 = x as Element of J by A4; n in dom (signature (A.x1)) by A1,Def14; then n in Seg len (signature (A.x1)) by FINSEQ_1:def 3; then n in Seg len (the charact of(A.x1)) by UNIALG_1:def 11; then n in dom (the charact of(A.x1)) by FINSEQ_1:def 3; then reconsider o = (the charact of A.x1).n as operation of A.x1 by UNIALG_2:6; f.x = o by A4; hence thesis; end; then reconsider f as ManySortedFunction of J by Def15; for j be Element of J holds f.j is homogeneous quasi_total non empty PartFunc of ((Carrier A).j)*,(Carrier A).j proof let j be Element of J; n in dom (signature (A.j)) by A1,Def14; then n in Seg len (signature (A.j)) by FINSEQ_1:def 3; then n in Seg len (the charact of(A.j)) by UNIALG_1:def 11; then n in dom (the charact of(A.j)) by FINSEQ_1:def 3; then reconsider o = (the charact of A.j).n as operation of A.j by UNIALG_2:6; ex R being 1-sorted st R = A.j & (Carrier A).j = the carrier of R by Def13; then f.j = o & (Carrier A).j = the carrier of A.j by A4; hence thesis; end; then reconsider f as ManySortedOperation of (Carrier A) by Def16; for i,j be Element of J holds arity (f.i) = arity (f.j) proof let i,j be Element of J; dom A = J by PBOOLE:def 3; then A5: signature A.i = signature A.j by Def12; A6: n in dom (signature (A.j)) by A1,Def14; then A7: n in Seg len (signature (A.j)) by FINSEQ_1:def 3; then n in Seg len (the charact of(A.j)) by UNIALG_1:def 11; then n in dom (the charact of(A.j)) by FINSEQ_1:def 3; then reconsider o = (the charact of A.j).n as operation of A.j by UNIALG_2 :6; A8: f.j = o by A4; A9: (signature A.j).n = arity (o) by A6,UNIALG_1:def 11; dom (f.j) = (arity (f.j))-tuples_on ((Carrier A).j) & dom o = (arity o)-tuples_on (the carrier of (A.j)) by UNIALG_2:2; then A10: arity (f.j) = arity o by A8,Th1; n in Seg len (the charact of(A.i)) by A5,A7,UNIALG_1:def 11; then n in dom (the charact of(A.i)) by FINSEQ_1:def 3; then reconsider o1 = (the charact of A.i).n as operation of A.i by UNIALG_2:6; A11: f.i = o1 by A4; A12: (signature A.i).n = arity (o1) by A5,A6,UNIALG_1:def 11; dom (f.i) = (arity (f.i))-tuples_on ((Carrier A).i) & dom o1 = (arity o1)-tuples_on (the carrier of A.i) by UNIALG_2:2; hence thesis by A5,A9,A10,A11,A12,Th1; end; then reconsider f as equal-arity ManySortedOperation of (Carrier A) by Th12; take f; let j be Element of J; let o be operation of A.j; assume (the charact of A.j).n = o; hence thesis by A4; end; uniqueness proof let O1,O2 be equal-arity ManySortedOperation of (Carrier A); assume A13: (for j be Element of J holds for o be operation of A.j st (the charact of A.j).n = o holds O1.j = o) & for j be Element of J holds for o be operation of A.j st (the charact of A.j).n = o holds O2.j = o; for x st x in J holds O1.x = O2.x proof let x; assume x in J; then reconsider x1 = x as Element of J; n in dom (signature (A.x1)) by A1,Def14; then n in Seg len (signature (A.x1)) by FINSEQ_1:def 3; then n in Seg len (the charact of(A.x1)) by UNIALG_1:def 11; then n in dom (the charact of(A.x1)) by FINSEQ_1:def 3; then reconsider o = (the charact of A.x1).n as operation of A.x1 by UNIALG_2:6; O1.x1 = o & O2.x1 = o by A13; hence thesis; end; hence thesis by PBOOLE:3; end; end; definition let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J; func ProdOpSeq(A) -> PFuncFinSequence of product Carrier A means :Def24: len it = len (ComSign A) & for n st n in dom it holds it.n = [[: ProdOp(A,n) :]]; existence proof defpred P[Nat,set] means $2 = [[: ProdOp(A,$1) :]]; set f = ComSign A; A1: for k st k in Seg len f ex x being Element of PFuncs((product Carrier A)*,product Carrier A) st P[k,x] proof let k; assume k in Seg len f; reconsider a = [[: ProdOp(A,k) :]] as Element of PFuncs((product Carrier A)*,product Carrier A) by PARTFUN1:119; take a; thus thesis; end; consider p being FinSequence of PFuncs((product Carrier A)*,product Carrier A) such that A2: dom p = Seg len f & for k st k in Seg len f holds P[k,p.k] from SeqDEx(A1); reconsider p as PFuncFinSequence of product Carrier A; take p; thus len p = len f by A2,FINSEQ_1:def 3; let n; assume n in dom p; hence thesis by A2; end; uniqueness proof let x,y be PFuncFinSequence of product Carrier A; assume A3:(len x = len (ComSign A) & for n st n in dom x holds x.n = [[: ProdOp(A,n) :]]) & len y = len (ComSign A) & for n st n in dom y holds y.n = [[: ProdOp(A,n) :]]; now let n; assume n in Seg len (ComSign A); then n in dom (ComSign A) & n in dom x & n in dom y by A3,FINSEQ_1:def 3; then x.n = [[: ProdOp(A,n) :]] & y.n = [[: ProdOp(A,n) :]] by A3; hence x.n = y.n; end; hence thesis by A3,FINSEQ_2:10; end; end; definition let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J; func ProdUnivAlg A -> strict Universal_Algebra equals UAStr (# product Carrier A, ProdOpSeq(A) #); coherence proof set ua = UAStr (# product Carrier A, ProdOpSeq(A) #), pr = product Carrier A; for n be Nat,h be PartFunc of pr*,pr st n in dom (the charact of ua) & h = (the charact of ua).n holds h is quasi_total proof let n be Nat,h be PartFunc of pr*,pr; assume A1: n in dom (the charact of ua) & (the charact of ua).n = h; then (the charact of ua).n = [[: ProdOp(A,n) :]] by Def24; hence h is quasi_total by A1; end; then A2: the charact of(ua) is quasi_total by UNIALG_1:def 5; for n be Nat,h be PartFunc of pr*,pr st n in dom (the charact of ua) & h = (the charact of ua).n holds h is homogeneous proof let n be Nat,h be PartFunc of pr*,pr; assume A3: n in dom (the charact of ua) & (the charact of ua).n = h; then (the charact of ua).n = [[: ProdOp(A,n) :]] by Def24; hence h is homogeneous by A3; end; then A4: the charact of(ua) is homogeneous by UNIALG_1:def 4; for n be set st n in dom (the charact of ua) holds (the charact of ua).n is non empty proof let n be set; assume A5: n in dom (the charact of ua); then reconsider n' = n as Nat; (the charact of ua).n = [[: ProdOp(A,n') :]] by A5,Def24; hence (the charact of ua).n is non empty; end; then A6: the charact of(ua) is non-empty by UNIALG_1:def 6; consider j be Element of J; A7: len the charact of(A.j) <> 0 by FINSEQ_1:25; len the charact of(ua) = len ComSign A by Def24 .= len(signature A.j) by Def14 .= len the charact of(A.j) by UNIALG_1:def 11; then the charact of(ua) <> {} by A7,FINSEQ_1:25; hence thesis by A2,A4,A6,UNIALG_1:def 7,def 8,def 9; end; end;

Back to top