:: Product of Family of Universal Algebras
:: by Beata Madras
::
:: Received October 12, 1993
:: Copyright (c) 1993-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies UNIALG_1, NAT_1, XBOOLE_0, FINSEQ_1, ZFMISC_1, MCART_1, RELAT_1,
FUNCT_1, FUNCT_2, PARTFUN1, FINSEQ_2, SUBSET_1, TARSKI, NUMBERS,
STRUCT_0, CQC_SIM1, UNIALG_2, PBOOLE, FUNCOP_1, RLVECT_2, CARD_3, CARD_1,
FINSEQ_4, FUNCT_5, PRALG_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
NAT_1, STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, FUNCT_2, BINOP_1, FUNCOP_1,
MCART_1, DOMAIN_1, PARTFUN1, FINSEQ_2, FUNCT_4, FUNCT_5, CARD_3,
MARGREL1, DTCONSTR, UNIALG_1, UNIALG_2, PBOOLE;
constructors BINOP_1, DOMAIN_1, FUNCT_4, FUNCT_5, CARD_3, PBOOLE, UNIALG_2,
DTCONSTR, STRUCT_0, RELSET_1, XTUPLE_0, NUMBERS;
registrations SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCOP_1,
FINSEQ_1, FINSEQ_2, CARD_3, PBOOLE, STRUCT_0, UNIALG_1, CARD_1, RELSET_1,
MARGREL1, XTUPLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, UNIALG_2, FUNCT_1, PBOOLE, XBOOLE_0, MARGREL1;
equalities UNIALG_2, XBOOLE_0, BINOP_1, FINSEQ_2, FUNCOP_1, ORDINAL1;
expansions TARSKI, UNIALG_2, FUNCT_1, PBOOLE, MARGREL1;
theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, FUNCOP_1, UNIALG_1,
DOMAIN_1, ZFMISC_1, MCART_1, UNIALG_2, FUNCT_2, FUNCT_5, CARD_3, FUNCT_4,
FINSEQ_3, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, MARGREL1, CARD_1,
XTUPLE_0;
schemes FINSEQ_1, PARTFUN1, FUNCT_2, FUNCT_1, CLASSES1;
begin
::
:: Product of Two Algebras
::
reserve U1,U2,U3 for Universal_Algebra,
n,m for Nat,
x,y,z for object,
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 MCART_1:def 12;
hence len f1 = len h1 by FINSEQ_3:29;
let n;
thus n in dom f1 implies f1.n = (h1.n)`1 by A1,A2,MCART_1:def 12;
end;
assume len f1 = len h1 & for n st n in dom f1 holds f1.n = (h1.n)`1;
then dom f1 = dom h1 &
for n being object st n in dom f1 holds f1.n = (h1.n)
`1 by FINSEQ_3:29;
hence thesis by MCART_1:def 12;
end;
coherence
proof
thus pr1 h1 is FinSequence of A;
end;
redefine 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
A3: f1 = pr2 h1;
then
A4: dom f1 = dom h1 by MCART_1:def 13;
hence len f1 = len h1 by FINSEQ_3:29;
let n;
thus n in dom f1 implies f1.n = (h1.n)`2 by A3,A4,MCART_1:def 13;
end;
assume len f1 = len h1 & for n st n in dom f1 holds f1.n = (h1.n)`2;
then dom f1 = dom h1 &
for n being object st n in dom f1 holds f1.n = (h1.n)
`2 by FINSEQ_3:29;
hence thesis by MCART_1:def 13;
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
set ar = (arity(f1))-tuples_on [:A,B:], ab = {s where s is Element of [:A,
B:]* : len s = arity(f1)};
defpred P[object,object] means
for h be FinSequence of [:A,B:] st $1 = h holds
$2 = [f1.(pr1 h),f2.(pr2 h)];
A2: dom f2 = (arity(f2))-tuples_on B by MARGREL1:22;
A3: rng f1 c= A & rng f2 c= B by RELAT_1:def 19;
A4: dom f1 = (arity(f1))-tuples_on A by MARGREL1:22;
A5: for x,y being object st x in ar & P[x,y] holds y in [:A,B:]
proof
let x,y be object;
assume that
A6: x in ar and
A7: P[x,y];
consider s being Element of [:A,B:]* such that
A8: x = s and
A9: len s = arity(f1) by A6;
reconsider s1 = pr1 s as Element of A* by FINSEQ_1:def 11;
len pr1 s = len s by Def1;
then s1 in {s3 where s3 is Element of A* : len s3 = arity(f1)} by A9;
then
A10: f1.s1 in rng f1 by A4,FUNCT_1:def 3;
reconsider s2 = pr2 s as Element of B* by FINSEQ_1:def 11;
len pr2 s = len s by Def2;
then s2 in {s3 where s3 is Element of B* : len s3 = arity(f2)} by A1,A9;
then
A11: f2.s2 in rng f2 by A2,FUNCT_1:def 3;
y = [f1.(pr1 s),f2.(pr2 s)] by A7,A8;
hence thesis by A3,A10,A11,ZFMISC_1:87;
end;
A12: for x,y,z being object st x in ar & P[x,y] & P[x,z] holds y = z
proof
let x,y,z be object;
assume that
A13: x in ar and
A14: P[x,y] and
A15: P[x,z];
consider s being Element of [:A,B:]* such that
A16: x = s and
len s = arity(f1) by A13;
y = [f1.(pr1 s),f2.(pr2 s)] by A14,A16;
hence thesis by A15,A16;
end;
consider f being PartFunc of ar,[:A,B:] such that
A17: for x being object holds x in dom f iff x in ar &
ex y being object st P[x,y] and
A18: for x being object st x in dom f holds P[x,f.x]
from PARTFUN1:sch 2(A5,A12);
A19: dom f = ar
proof
thus dom f c= ar
by A17;
let x be object;
assume
A20: x in ar;
then consider s being Element of [:A,B:]* such that
A21: x = s and
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 A21;
end;
hence thesis by A17,A20;
end;
ar in the set of all i-tuples_on [:A,B:] where i is Nat;
then ar c= union the set of all i-tuples_on [:A,B:] where i is Nat
by ZFMISC_1:74;
then ar c= [:A,B:]* by FINSEQ_2:108;
then reconsider f as PartFunc of [:A,B:]*,[:A,B:] by RELSET_1:7;
A22: f is quasi_total
proof
let x,y be FinSequence of [:A,B:];
assume that
A23: len x = len y and
A24: x in dom f;
reconsider y9 = y as Element of [:A,B:]* by FINSEQ_1:def 11;
ex s1 being Element of [:A,B:]* st s1 = x & len s1 = arity(f1) by A19,A24
;
then y9 in ab by A23;
hence thesis by A19;
end;
f is homogeneous
proof
let x,y be FinSequence;
assume x in dom f & y in dom f;
then (ex s1 being Element of [:A,B:]* st s1 = x & len s1 = arity(f1) )&
ex s2 being Element of [:A,B:]* st s2 = y & len s2 = arity(f1) by A19;
hence thesis;
end;
then reconsider
f as homogeneous quasi_total non empty PartFunc of ([:A,B:])*,
[:A,B:] by A19,A22;
take f;
thus dom f = ar by A19;
let h be FinSequence of [:A,B:];
assume h in dom f;
hence thesis by A18;
end;
uniqueness
proof
let x,y be homogeneous quasi_total non empty PartFunc of ([:A,B:])* ,[:A,B
:];
assume that
A25: dom x = (arity(f1))-tuples_on [:A,B:] and
A26: for h be FinSequence of [:A,B:] st h in dom x holds x.h = [f1.(
pr1 h),f2.(pr2 h)] and
A27: dom y = (arity(f1))-tuples_on [:A,B:] and
A28: 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 c9 = c as FinSequence of [:A,B:];
assume
A29: c in dom x;
then x.c9 = [f1.(pr1 c9),f2.(pr2 c9)] by A26;
hence x.c = y.c by A25,A27,A28,A29;
end;
hence thesis by A25,A27,PARTFUN1:5;
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
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:]];
set l = len the charact of(U1), c = [:the carrier of U1,the carrier of U2
:];
A2: dom the charact of(U2) = Seg len the charact of(U2) by FINSEQ_1:def 3;
A3: Seg l = dom the charact of(U1) by FINSEQ_1:def 3;
A4: for m being Nat st m in Seg l ex x being Element of PFuncs(c*,c) st P[ m,x]
proof
let m be Nat;
assume
A5: 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 A3,MARGREL1:def 24
,UNIALG_1:1;
len the charact of(U1) = len the charact of(U2) by A1,UNIALG_2:1;
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,A5,
MARGREL1:def 24,UNIALG_1:1;
reconsider F = [[:f1,f2:]] as Element of PFuncs(c*,c) by PARTFUN1:45;
take F;
let h1,h2;
assume h1=(the charact of(U1)).m & h2=(the charact of(U2)).m;
hence thesis;
end;
consider p be FinSequence of PFuncs(c*,c) such that
A6: dom p = Seg l and
A7: for m being Nat st m in Seg l holds P[m,p.m] from FINSEQ_1:sch 5(
A4);
reconsider p as PFuncFinSequence of c;
take p;
thus len p = len the charact of(U1) by A6,FINSEQ_1:def 3;
let n;
assume n in dom p;
hence thesis by A6,A7;
end;
uniqueness
proof
let x,y be PFuncFinSequence of [:the carrier of U1,the carrier of U2:];
assume that
A8: len x = len the charact of(U1) and
A9: 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
A10: len y = len the charact of(U1) and
A11: 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:]];
A12: dom x = Seg len the charact of(U1) by A8,FINSEQ_1:def 3;
now
let m be Nat;
assume
A13: m in dom x;
then m in dom the charact of(U1) by A12,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 MARGREL1:def 24
,UNIALG_1:1;
Seg len the charact of(U2) = Seg len the charact of(U1) by A1,UNIALG_2:1;
then m in dom the charact of(U2) by A12,A13,FINSEQ_1:def 3;
then reconsider h2=(the charact of(U2)).m as homogeneous quasi_total non
empty PartFunc of (the carrier of U2)*,the carrier of U2 by MARGREL1:def 24
,UNIALG_1:1;
m in dom y & x.m = [[:h1,h2:]] by A9,A10,A12,A13,FINSEQ_1:def 3;
hence x.m = y.m by A11;
end;
hence thesis by A8,A10,FINSEQ_2:9;
end;
end;
theorem Th1:
U1,U2 are_similar implies UAStr (# [:the carrier of U1,the
carrier of U2:], Opers(U1,U2) #) is strict Universal_Algebra
proof
set C = UAStr(# [:the carrier of U1,the carrier of U2:], Opers(U1,U2) #);
A1: dom Opers(U1,U2) = Seg len Opers(U1,U2) by FINSEQ_1:def 3;
assume
A2: U1,U2 are_similar;
then
A3: dom the charact of(U2) = Seg len the charact of(U2) & len the charact of
(U2) = len the charact of(U1) by FINSEQ_1:def 3,UNIALG_2:1;
A4: len Opers(U1,U2) = len the charact of(U1) by A2,Def4;
A5: dom the charact of(U1) = Seg len the charact of(U1) by FINSEQ_1:def 3;
A6: the charact of(C) is quasi_total
proof
let n;
let h be PartFunc of (the carrier of C)*,(the carrier of C);
assume that
A7: n in dom the charact of(C) and
A8: h = (the charact of(C)).n;
reconsider h2=(the charact of(U2)).n as homogeneous quasi_total non empty
PartFunc of (the carrier of U2)*,the carrier of U2 by A1,A4,A3,A7,
MARGREL1:def 24,UNIALG_1:1;
reconsider h1=(the charact of U1).n as homogeneous quasi_total non empty
PartFunc of (the carrier of U1)*,the carrier of U1 by A1,A5,A4,A7,
MARGREL1:def 24,UNIALG_1:1;
h = [[:h1,h2:]] by A2,A7,A8,Def4;
hence thesis;
end;
A9: the charact of(C) is non-empty
proof
let n be object;
set h = (the charact of(C)).n;
assume
A10: n in dom the charact of(C);
then reconsider m = n as Element of NAT;
reconsider h2=(the charact of(U2)).m as homogeneous quasi_total non empty
PartFunc of (the carrier of U2)*,the carrier of U2 by A1,A4,A3,A10,
MARGREL1:def 24,UNIALG_1:1;
reconsider h1=(the charact of(U1)).m as homogeneous quasi_total non empty
PartFunc of (the carrier of U1)*,the carrier of U1 by A1,A5,A4,A10,
MARGREL1:def 24,UNIALG_1:1;
h = [[:h1,h2:]] by A2,A10,Def4;
hence thesis;
end;
A11: the charact of(C) is homogeneous
proof
let n;
let h be PartFunc of (the carrier of C)*,the carrier of C;
assume that
A12: n in dom the charact of(C) and
A13: h = (the charact of(C)).n;
reconsider h2=(the charact of(U2)).n as homogeneous quasi_total non empty
PartFunc of (the carrier of U2)*,the carrier of U2 by A1,A4,A3,A12,
MARGREL1:def 24,UNIALG_1:1;
reconsider h1=(the charact of(U1)).n as homogeneous quasi_total non empty
PartFunc of (the carrier of U1)*,the carrier of U1 by A1,A5,A4,A12,
MARGREL1:def 24,UNIALG_1:1;
h = [[:h1,h2:]] by A2,A12,A13,Def4;
hence thesis;
end;
the charact of(C) <> {} by A4;
hence thesis by A6,A11,A9,UNIALG_1:def 1,def 2,def 3;
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,Th1;
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 FUNCT_2:sch 4;
end;
uniqueness
proof
let f,g be Function of [:A,B:],[:B,A:];
assume that
A1: for a be Element of [:A,B:] holds f.a = [a`2,a`1] and
A2: 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] by A1;
hence f.a = g.a by A2;
end;
hence thesis by FUNCT_2:63;
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 be object;
A1: dom Inv (A,B) = [:A,B:] by FUNCT_2:def 1;
assume x in [:B,A:];
then reconsider y = x as Element of [:B,A:];
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]
.= [y`1,y`2]
.= y by MCART_1:21;
hence thesis by A1,FUNCT_1:def 3;
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 be object;
assume that
A1: x in dom Inv(A,B) & y in dom Inv(A,B) and
A2: Inv(A,B).x = Inv(A,B).y;
reconsider x1 = x,y1 = y as Element of [:A,B:] by A1,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 A2,XTUPLE_0:1;
hence thesis by DOMAIN_1:2;
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 Th5:
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;
A2: dom Opers(U1,U2) = Seg len Opers(U1,U2) by FINSEQ_1:def 3;
A3: dom the charact of(U1) = Seg len the charact of(U1) by FINSEQ_1:def 3;
let o1 be operation of U1,o2 be operation of U2,o be operation of [:U1,U2:],
n be Nat;
assume that
A4: o1 = (the charact of U1).n and
A5: o2 = (the charact of U2).n and
A6: o = (the charact of [:U1,U2:]).n and
A7: n in dom the charact of(U1);
A8: dom (signature U1) = Seg len (signature U1) & len signature U1 = len
the charact of (U1) by FINSEQ_1:def 3,UNIALG_1:def 4;
then
A9: (signature U1).n = arity o1 by A4,A7,A3,UNIALG_1:def 4;
A10: signature U1 = signature U2 by A1;
then
A11: (signature U2).n = arity o2 by A5,A7,A3,A8,UNIALG_1:def 4;
A12: [:U1,U2:] = UAStr (# [:the carrier of U1,the carrier of U2:], Opers(U1,
U2) #) & len the charact of(U1) = len Opers(U1,U2) by A1,Def4,Def5;
then o = [[:o1,o2:]] by A1,A4,A5,A6,A7,A3,A2,Def4;
then
A13: dom o = (arity o1)-tuples_on [:the carrier of U1,the carrier of U2:] by
A10,A9,A11,Def3;
(ex x being FinSequence st x in dom o) & for x be FinSequence st x in
dom o holds len x = arity o1
proof
set a = the Element of (arity o1)-tuples_on [:the carrier of U1,the carrier of
U2:];
a in dom o by A13;
hence ex x being FinSequence st x in dom o;
let x be FinSequence;
assume x in dom o;
then ex s be Element of ([:the carrier of U1,the carrier of U2:]) * st s =
x & len s = arity o1 by A13;
hence thesis;
end;
hence thesis by A1,A4,A5,A6,A7,A3,A2,A12,A9,A11,Def4,MARGREL1:def 25;
end;
theorem
U1,U2 are_similar implies [:U1,U2:],U1 are_similar
proof
A1: dom signature(U1) = Seg len signature(U1) by FINSEQ_1:def 3;
A2: dom signature(U1) = Seg len signature(U1) by FINSEQ_1:def 3;
A3: dom the charact of([:U1,U2:]) = Seg len the charact of([:U1,U2:]) by
FINSEQ_1:def 3;
A4: dom the charact of(U2) = Seg len the charact of(U2) by FINSEQ_1:def 3;
A5: dom the charact of(U1) = Seg len the charact of(U1) by FINSEQ_1:def 3;
assume
A6: 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 A6,Def4;
then
A7: len signature ([:U1,U2:]) = len the charact of(U1) by UNIALG_1:def 4
.= len signature(U1) by UNIALG_1:def 4;
A8: dom signature([:U1,U2:]) = Seg len signature([:U1,U2:]) by FINSEQ_1:def 3;
now
let n be Nat;
assume
A9: n in dom signature(U1);
then n in dom the charact of([:U1,U2:]) by A7,A1,A3,UNIALG_1:def 4;
then reconsider
o12 = (the charact of [:U1,U2:]).n as operation of [:U1,U2:] by
FUNCT_1:def 3;
len signature(U1) = len signature(U2) by A6
.= len the charact of(U2) by UNIALG_1:def 4;
then reconsider
o2 = (the charact of U2).n as operation of U2 by A1,A4,A9,FUNCT_1:def 3;
A10: o2 = (the charact of U2).n;
A11: n in Seg len the charact of(U1) by A2,A9,UNIALG_1:def 4;
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
FUNCT_1:def 3;
(signature(U1)).n = arity(o1) & (signature([:U1,U2:])).n = arity(o12)
by A7,A1,A8,A9,UNIALG_1:def 4;
hence (signature(U1)).n = (signature([:U1,U2:])).n by A6,A5,A11,A10,Th5;
end;
then signature(U1) = signature([:U1,U2:]) by A7,FINSEQ_2:9;
hence thesis;
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 that
A1: U1 is SubAlgebra of U2 and
A2: U3 is SubAlgebra of U4 and
A3: U2,U4 are_similar;
A4: [:U2,U4:] = UAStr (# [:the carrier of U2,the carrier of U4:], Opers(U2,
U4) #) by A3,Def5;
A5: U1,U2 are_similar by A1,UNIALG_2:13;
then
A6: U1,U4 are_similar by A3;
A7: U3,U4 are_similar by A2,UNIALG_2:13;
then
A8: [: U1,U3:] = UAStr (# [:the carrier of U1,the carrier of U3:], Opers(U1,
U3) #) by A6,Def5,UNIALG_2:2;
A9: the carrier of U1 is Subset of U2 & the carrier of U3 is Subset of U4
by A1,A2,UNIALG_2:def 7;
hence the carrier of [:U1,U3:] is Subset of [:U2,U4:] by A8,A4,ZFMISC_1:96;
let B be non empty Subset of [:U2,U4:];
assume
A10: B = the carrier of [:U1,U3:];
signature (U4) = signature (U2) by A3;
then len the charact of(U4) = len signature(U2) by UNIALG_1:def 4;
then
A11: dom the charact of(U4) = Seg len the charact of(U4) & len the charact
of(U4) = len the charact of(U2) by FINSEQ_1:def 3,UNIALG_1:def 4;
A12: dom the charact of(U1) = Seg len the charact of(U1) by FINSEQ_1:def 3;
A13: dom the charact of(U2) = Seg len the charact of(U2) by FINSEQ_1:def 3;
A14: U1,U3 are_similar by A7,A6;
then
A15: len the charact of([:U1,U3:]) = len the charact of(U1) by A8,Def4;
signature (U1) = signature (U3) by A14;
then len the charact of(U1) = len signature(U3) by UNIALG_1:def 4;
then
A16: dom the charact of(U3) = Seg len the charact of(U3) & len the charact
of(U1) = len the charact of(U3) by FINSEQ_1:def 3,UNIALG_1:def 4;
A17: dom Opers([:U2,U4:],B) = Seg len Opers([:U2,U4:],B) by FINSEQ_1:def 3;
A18: dom the charact of([:U2,U4:]) = dom Opers([:U2,U4:],B) by UNIALG_2:def 6;
then len the charact of([:U2,U4:]) = len Opers([:U2,U4:],B) by FINSEQ_3:29;
then
A19: len the charact of(U2) = len Opers([:U2,U4:],B) by A3,A4,Def4;
signature (U1) = signature (U2) by A5;
then len the charact of(U1) = len signature(U2) by UNIALG_1:def 4;
then
A20: len the charact of([:U1,U3:]) = len Opers([:U2,U4:],B) by A19,A15,
UNIALG_1:def 4;
reconsider B3 = the carrier of U3 as non empty Subset of U4 by A2,
UNIALG_2:def 7;
A21: B3 is opers_closed by A2,UNIALG_2:def 7;
reconsider B1 = the carrier of U1 as non empty Subset of U2 by A1,
UNIALG_2:def 7;
A22: B1 is opers_closed by A1,UNIALG_2:def 7;
A23: [:the carrier of U1,the carrier of U3:] c= [:the carrier of U2,the
carrier of U4:] by A9,ZFMISC_1:96;
A24: 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;
reconsider s0 = s as Element of ([:the carrier of U1,the carrier of U3:])*
by A8,A10,FINSEQ_1:def 11;
consider n be Nat such that
A25: n in dom the charact of([:U2,U4:]) and
A26: (the charact of [:U2,U4:]).n = o by FINSEQ_2:10;
reconsider s3 = pr2 s0 as Element of B3* by FINSEQ_1:def 11;
reconsider s1 = pr1 s0 as Element of B1* by FINSEQ_1:def 11;
A27: len the charact of([:U2,U4:]) = len the charact of(U2) by A3,A4,Def4;
A28: n in Seg len the charact of ([:U2,U4:]) by A25,FINSEQ_1:def 3;
then
A29: n in dom the charact of(U2) by A27,FINSEQ_1:def 3;
then reconsider o2 = (the charact of U2).n as operation of U2 by
FUNCT_1:def 3;
len the charact of(U4) = len the charact of(U2) by A3,UNIALG_2:1;
then n in dom the charact of(U4) by A28,A27,FINSEQ_1:def 3;
then reconsider o4 = (the charact of U4).n as operation of U4 by
FUNCT_1:def 3;
A30: o = [[:o2,o4:]] by A3,A26,A29,Th5;
o4 = (the charact of U4).n;
then
A31: arity o = arity o2 by A3,A26,A29,Th5;
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 A23;
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;
o2 = (the charact of U2).n;
then
A32: arity o = arity o4 by A3,A26,A29,Th5;
assume
A33: len s = arity o;
then
A34: ss in {w where w is Element of ([:the carrier of U2,the carrier of U4
:] )* : len w = arity o2 } by A31;
B3 is_closed_on o4 & len s3 = len s0 by A21,Def2;
then
A35: o4.s3 in B3 by A33,A32;
B1 is_closed_on o2 & len s1 = len s0 by A22,Def1;
then
A36: o2.s1 in B1 by A33,A31;
dom [[:o2,o4:]]=(arity(o2))-tuples_on [:the carrier of U2,the carrier
of U4:] by A31,A32,Def3;
then o.s = [o2.(pr1 ss),o4.(pr2 ss)] by A31,A32,A30,A34,Def3;
hence thesis by A8,A10,A36,A35,ZFMISC_1:87;
end;
A37: dom the charact of(U4) = dom Opers(U4,B3) by UNIALG_2:def 6;
A38: dom the charact of([:U1,U3:]) = Seg len the charact of([:U1,U3:]) by
FINSEQ_1:def 3;
A39: dom the charact of(U2) = dom Opers(U2,B1) by UNIALG_2:def 6;
for n being Nat st n in dom the charact of([:U1,U3:]) holds (the
charact of [:U1,U3:]).n = Opers([:U2,U4:],B).n
proof
let n be Nat;
assume
A40: n in dom the charact of([:U1,U3:]);
then reconsider
o2 = (the charact of U2).n as operation of U2 by A19,A20,A13,A38,
FUNCT_1:def 3;
reconsider o4 = (the charact of U4).n as operation of U4 by A19,A20,A38,A11
,A40,FUNCT_1:def 3;
reconsider o24 = (the charact of [:U2,U4:]).n as operation of [:U2,U4:] by
A18,A20,A38,A17,A40,FUNCT_1:def 3;
A41: o24 = [[:o2,o4:]] by A3,A19,A20,A13,A38,A40,Th5;
reconsider o3 = (the charact of U3).n as operation of U3 by A15,A38,A16,A40
,FUNCT_1:def 3;
Opers(U4,B3).n = o4/.B3 by A19,A20,A38,A11,A37,A40,UNIALG_2:def 6;
then
A42: o3 = o4/.B3 by A2,UNIALG_2:def 7;
o2 = (the charact of U2).n;
then
A43: arity o24 = arity o4 by A3,A19,A20,A13,A38,A40,Th5;
reconsider o1 = (the charact of U1).n as operation of U1 by A15,A12,A38,A40
,FUNCT_1:def 3;
Opers(U2,B1).n = o2/. B1 by A19,A20,A13,A38,A39,A40,UNIALG_2:def 6;
then
A44: o1 = o2/.B1 by A1,UNIALG_2:def 7;
A45: B3 is_closed_on o4 by A21;
then
A46: arity (o4/.B3) = arity o4 by UNIALG_2:5;
o4 = (the charact of U4).n;
then
A47: arity o24 = arity o2 by A3,A19,A20,A13,A38,A40,Th5;
then
A48: dom ([[:o2,o4:]]|((arity o24)-tuples_on B)) = dom ([[:o2,o4:]]) /\ ((
arity o2)-tuples_on B) by RELAT_1:61
.= (arity o2)-tuples_on (the carrier of [:U2,U4:]) /\ ((arity o2)
-tuples_on B) by A4,A43,A47,Def3
.= ((arity o2)-tuples_on B) by MARGREL1:21;
A49: B1 is_closed_on o2 by A22;
then
A50: arity (o2/.B1) = arity o2 by UNIALG_2:5;
then
A51: dom ([[:o2/.B1,o4/.B3:]]) = (arity o2)-tuples_on B by A8,A10,A43,A47,A46
,Def3;
A52: now
let x be object;
A53: dom ([[:o2,o4:]]|((arity o24)-tuples_on B)) c= dom [[:o2,o4:]] by
RELAT_1:60;
assume
A54: x in ((arity o2)-tuples_on B);
then consider s be Element of B* such that
A55: s = x and
A56: len s = arity o2;
rng s c= B by FINSEQ_1:def 4;
then rng s c= [:the carrier of U2,the carrier of U4:] by A4,XBOOLE_1:1;
then reconsider
s0 = s as FinSequence of [:the carrier of U2,the carrier of
U4:] by FINSEQ_1:def 4;
A57: ([[:o2,o4:]]|((arity o24)-tuples_on B)).x = [[:o2,o4:]].s0 by A48,A54,A55
,FUNCT_1:47
.= [o2.(pr1 s0),o4.(pr2 s0)] by A43,A47,A48,A54,A55,A53,Def3;
reconsider s1 = s as FinSequence of [:B1 qua non empty set,B3 qua non
empty set:] by A8,A10;
reconsider s11 = pr1 s1 as Element of B1* by FINSEQ_1:def 11;
len (pr1 s1) = len s1 by Def1;
then
A58: s11 in {a where a is Element of B1 *: len a = arity o2} by A56;
reconsider s12 = pr2 s1 as Element of B3* by FINSEQ_1:def 11;
len (pr2 s1) = len s1 by Def2;
then
A59: s12 in {b where b is Element of B3*: len b = arity o4} by A43,A47,A56;
A60: dom (o4|(arity o4)-tuples_on B3) = dom o4 /\ (arity o4)-tuples_on
B3 by RELAT_1:61
.= ((arity o4)-tuples_on the carrier of U4) /\ (arity o4)-tuples_on
B3 by MARGREL1:22
.= (arity o4)-tuples_on B3 by MARGREL1:21;
A61: dom (o2|(arity o2)-tuples_on B1) = dom o2 /\ (arity o2)-tuples_on
B1 by RELAT_1:61
.= ((arity o2)-tuples_on the carrier of U2) /\ (arity o2)-tuples_on
B1 by MARGREL1:22
.= (arity o2)-tuples_on B1 by MARGREL1:21;
[[:o2/.B1,o4/.B3:]].x = [(o2/.B1).(pr1 s1),(o4/.B3).(pr2 s1)] by A43,A47
,A50,A46,A51,A54,A55,Def3
.= [(o2|((arity o2)-tuples_on B1)).s11,(o4/.B3).(pr2 s1)] by A49,
UNIALG_2:def 5
.= [o2.(pr1 s1),(o4/.B3).(pr2 s1)] by A58,A61,FUNCT_1:47
.= [o2.(pr1 s1),(o4|((arity o4)-tuples_on B3)).(pr2 s1)] by A45,
UNIALG_2:def 5
.= [o2.(pr1 s1),o4.(pr2 s1)] by A59,A60,FUNCT_1:47;
hence [[:o2/.B1,o4/.B3:]].x = ([[:o2,o4:]]|((arity o24)-tuples_on B)).x
by A57;
end;
thus Opers([:U2,U4:],B).n = o24/.B by A20,A38,A17,A40,UNIALG_2:def 6
.= [[:o2,o4:]]|((arity o24)-tuples_on B) by A24,A41,UNIALG_2:def 5
.= [[:o2/.B1,o4/.B3:]] by A51,A48,A52
.= (the charact of [:U1,U3:]).n by A14,A8,A40,A44,A42,Def4;
end;
hence thesis by A24,A20,FINSEQ_2:9;
end;
begin
::
:: Trivial Algebra
::
definition
let k be Nat;
func TrivialOp(k) -> PartFunc of {{}}*,{{}} means
:Def7:
dom it = { k |-> {} } & rng it = {{}};
existence
proof
consider f be Function such that
A1: dom f = {k |-> {}} and
A2: rng f = {{}} by FUNCT_1:5;
dom f c= {{}}*
proof
reconsider a = {} as Element of {{}} by TARSKI:def 1;
let x be object;
assume x in dom f;
then x = k |-> a by A1,TARSKI:def 1;
hence thesis by FINSEQ_1:def 11;
end;
then reconsider f as PartFunc of {{}}*,{{}} by A2,RELSET_1:4;
take f;
thus thesis by A1,A2;
end;
uniqueness by FUNCT_1:7;
end;
registration
let k be Nat;
cluster TrivialOp k -> homogeneous quasi_total non empty;
coherence
proof
set f = TrivialOp k;
A1: dom f = {k |-> {}} by Def7;
thus f is homogeneous
by A1;
now
let x,y be FinSequence of {{}};
assume that
A2: len x = len y and
A3: x in dom f;
A4: dom x = Seg len x by FINSEQ_1:def 3;
A5: x = k |-> {} by A1,A3,TARSKI:def 1;
now
let n be Nat;
assume
n in dom x;
then n in dom y by A2,A4,FINSEQ_1:def 3;
then
A6: y.n in {{}} by FINSEQ_2:11;
x.n = {} by A5;
hence x.n = y.n by A6,TARSKI:def 1;
end;
hence y in dom f by A2,A3,FINSEQ_2:9;
end;
hence thesis by A1;
end;
end;
theorem
for k being Nat holds arity TrivialOp(k) = k
proof
let k be Nat;
now
dom TrivialOp(k) = {k |-> {}} by Def7;
then k |-> {} in dom TrivialOp(k) by TARSKI:def 1;
hence ex x being FinSequence st x in dom TrivialOp(k);
let x be FinSequence;
assume x in dom TrivialOp(k);
then x in {k |-> {}} by Def7;
then x = k |-> {} by TARSKI:def 1;
hence len x = k by CARD_1:def 7;
end;
hence thesis by MARGREL1:def 25;
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 being Nat st k in Seg len f ex x being Element of PFuncs({{}}*,{
{}}) st P[k,x]
proof
let k be Nat;
assume k in Seg len f;
then k in dom f by FINSEQ_1:def 3;
then reconsider k1 = f.k as Element of NAT by FINSEQ_2:11;
reconsider A = TrivialOp(k1) as Element of PFuncs({{}}*,{{}}) by
PARTFUN1:45;
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 being Nat st k in Seg len f holds P[k,p.
k] from FINSEQ_1:sch 5(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 that
A3: len x=len f and
A4: for n st n in dom x for m st m = f.n holds x.n=TrivialOp (m) and
A5: len y=len f and
A6: for n st n in dom y for m st m = f.n holds y.n= TrivialOp(m);
A7: dom x = Seg len f by A3,FINSEQ_1:def 3;
now
let n be Nat;
assume
A8: n in dom x;
then n in dom f by A7,FINSEQ_1:def 3;
then reconsider m = f.n as Element of NAT by FINSEQ_2:11;
n in dom y & x.n=TrivialOp(m) by A4,A5,A7,A8,FINSEQ_1:def 3;
hence x.n = y.n by A6;
end;
hence thesis by A3,A5,FINSEQ_2:9;
end;
end;
theorem Th9:
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 quasi_total
proof
let n be Nat,h be PartFunc of {{}}*,{{}};
assume that
A2: n in dom TrivialOps(f) and
A3: (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 Element of NAT by A2,FINSEQ_2:11;
(TrivialOps(f)).n = TrivialOp(m) by A2,Def8;
hence thesis by A3;
end;
A4: for n be object st n in dom TrivialOps(f)
holds (TrivialOps(f)).n is non empty
proof
let n be object;
assume
A5: n in dom TrivialOps(f);
then reconsider k = n as Element of 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 Element of NAT by A5,FINSEQ_2:11;
(TrivialOps(f)).k = TrivialOp(m) by A5,Def8;
hence thesis;
end;
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 that
A6: n in dom TrivialOps(f) and
A7: (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 Element of NAT by A6,FINSEQ_2:11;
(TrivialOps(f)).n = TrivialOp(m) by A6,Def8;
hence thesis by A7;
end;
hence thesis by A1,A4;
end;
theorem Th10:
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 Th9;
len (the charact of U0) = len f by Def8;
then the charact of U0 <> {} by A1;
hence thesis by A2,UNIALG_1:def 1,def 2,def 3;
end;
registration
let D be non empty set;
cluster non empty for Element of D*;
existence
proof
set d = the Element of D;
reconsider e = <*d*> as Element of D* by FINSEQ_1:def 11;
take e;
thus 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 Th10;
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;
registration
cluster Univ_Alg-yielding for Function;
existence
proof
reconsider f = {} as Function;
take f;
let x;
thus thesis;
end;
end;
registration
cluster Univ_Alg-yielding -> 1-sorted-yielding for Function;
coherence;
end;
registration
let I be set;
cluster 1-sorted-yielding for ManySortedSet of I;
existence
proof
set A = the 1-sorted;
set f = I --> A;
A1: dom f = I by FUNCOP_1:13;
reconsider f as ManySortedSet of I;
take f;
for i be set st i in dom f holds f.i is 1-sorted by A1,FUNCOP_1:7;
hence thesis;
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;
registration
let J be non empty set;
cluster equal-signature Univ_Alg-yielding for ManySortedSet of J;
existence
proof
set U1 = the Universal_Algebra;
set f = J --> U1;
A1: dom f = J by FUNCOP_1:13;
reconsider f as ManySortedSet of J;
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 that
A2: x in dom f and
A3: y in dom f;
let U2,U3;
assume
A4: U2 = f.x & U3 = f.y;
f.x = U1 by A1,A2,FUNCOP_1:7;
hence thesis by A1,A3,A4,FUNCOP_1:7;
end;
hence f is equal-signature;
for x st x in dom f holds f.x is Universal_Algebra by A1,FUNCOP_1:7;
hence thesis;
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 PARTFUN1:def 2;
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 PARTFUN1:def 2;
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[object,object] means
ex R being 1-sorted st R = A.$1 & $2 = the carrier of R;
A1: for i be object st i in J ex j be object st P[i,j]
proof
let i be object;
assume
A2: i in J;
then reconsider J as non empty set;
reconsider i9 = i as Element of J by A2;
reconsider B = A as 1-sorted-yielding ManySortedSet of J;
take the carrier of B.i9, B.i9;
thus thesis;
end;
consider M being Function such that
A3: dom M = J and
A4: for i being object st i in J holds P[i,M.i] from CLASSES1:sch 1(A1);
reconsider M as ManySortedSet of J by A3,PARTFUN1:def 2,RELAT_1:def 18;
take M;
thus thesis by A4;
end;
uniqueness
proof
let X,Y be ManySortedSet of J;
assume
A5: ( for j be set st j in J ex R being 1-sorted st R = A.j & X.j =
the carrier of R)& 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 object st i in J holds X.i = Y.i
proof
let i be object;
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;
hence thesis;
end;
hence thesis;
end;
end;
registration
let J be non empty set, A be Univ_Alg-yielding ManySortedSet of J;
cluster Carrier A -> non-empty;
coherence
proof
let i be object;
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 PARTFUN1:def 2;
then R is Universal_Algebra by A1,A2,Def10;
hence thesis by A3;
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
set j = the Element of J;
reconsider U0 = A.j as Universal_Algebra;
take signature U0;
let j1 be Element of J;
dom A = J by PARTFUN1:def 2;
hence thesis by Def12;
end;
uniqueness
proof
set j = the Element of J;
let X,Y be FinSequence of NAT;
assume that
A1: for j be Element of J holds X = signature (A.j) and
A2: for j be Element of J holds Y = signature (A.j);
reconsider U0 = A.j as Universal_Algebra;
X = signature U0 by A1;
hence thesis by A2;
end;
end;
registration
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
:Def15:
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[object,object] means $2 in B.$1;
A1: for x being object st x in J
ex y being object st P[x,y]
by XBOOLE_0:def 1;
consider f be Function such that
A2: dom f = J &
for x being object st x in J holds P[x,f.x] from CLASSES1:sch 1(A1);
deffunc G(object) = <*>(B.$1) .--> f.$1;
consider F being Function such that
A3: dom F = J &
for x being object st x in J holds F.x = G(x) from FUNCT_1:sch 3;
reconsider F as ManySortedSet of J by A3,PARTFUN1:def 2,RELAT_1:def 18;
for x being object st x in dom F holds F.x is Function
proof
let x be object;
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 FUNCOP_1:def 6;
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 MARGREL1:18;
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 Def15;
end;
definition
let IT be Function;
attr IT is equal-arity means
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;
registration
let J be non empty set, B be non-empty ManySortedSet of J;
cluster equal-arity for ManySortedOperation of B;
existence
proof
defpred P[object,object] means $2 in B.$1;
A1: for x being object st x in J
ex y being object st P[x,y]
by XBOOLE_0:def 1;
consider f be Function such that
A2: dom f = J &
for x being object st x in J holds P[x,f.x] from CLASSES1:sch 1(A1);
deffunc G(object) = <*>(B.$1) .--> f.$1;
consider F being Function such that
A3: dom F = J &
for x being object st x in J holds F.x = G(x) from FUNCT_1:sch 3;
reconsider F as ManySortedSet of J by A3,PARTFUN1:def 2,RELAT_1:def 18;
for x being object st x in dom F holds F.x is Function
proof
let x be object;
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 FUNCOP_1:def 6;
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
MARGREL1:18;
end;
then reconsider F as ManySortedOperation of B by Def15;
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 be set;
assume that
A4: x in dom F and
A5: y in dom F;
reconsider x1 = x, y1 = y as Element of J by A3,A4,A5;
let g,h be Function;
assume that
A6: F.x = g and
A7: F.y = h;
reconsider fx = f.x1 as Element of B.x1 by A2;
let n,m be Nat;
let X,Y be non empty set;
assume that
dom g = n-tuples_on X and
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 that
A8: g = o1 and
A9: h = o2;
reconsider o1x = <*>(B.x1) .--> fx as homogeneous quasi_total non empty
PartFunc of (B.x1)*,B.x1 by MARGREL1:18;
A10: dom o1x = {{}(B.x1)} by FUNCOP_1:13;
consider p1 be object such that
A11: p1 in dom o1 by XBOOLE_0:def 1;
dom o1 c= X* by RELAT_1:def 18;
then reconsider p1 as Element of X* by A11;
o1 = <*>(B.x) .--> f.x by A3,A4,A6,A8;
then p1 = <*>(B.x1) by A10,A11,TARSKI:def 1;
then len p1 = 0;
then
A12: arity o1 = 0 by A11,MARGREL1:def 25;
reconsider fy = f.y1 as Element of B.y1 by A2;
reconsider o2y = <*>(B.y1) .--> fy as homogeneous quasi_total non empty
PartFunc of (B.y1)*,B.y1 by MARGREL1:18;
A13: dom o2y = {{}(B.y1)} by FUNCOP_1:13;
consider p2 be object such that
A14: p2 in dom o2 by XBOOLE_0:def 1;
dom o2 c= Y* by RELAT_1:def 18;
then reconsider p2 as Element of Y* by A14;
o2 = <*>(B.y) .--> f.y by A3,A5,A7,A9;
then p2 = <*>(B.y1) by A13,A14,TARSKI:def 1;
then len p2 = 0;
hence thesis by A12,A14,MARGREL1:def 25;
end;
hence thesis;
end;
end;
theorem Th11:
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) = arity(O.j)-tuples_on (B.j) by MARGREL1:22;
dom O = J & dom (O.i) = arity(O.i)-tuples_on (B.i) by MARGREL1:22
,PARTFUN1:def 2;
hence thesis by A1,A2;
end;
assume
A3: for i,j be Element of J holds arity (O.i) = arity (O.j);
let x,y be set;
assume x in dom O & y in dom O;
then reconsider x1 = x, y1 = y as Element of J by PARTFUN1:def 2;
let f,g be Function;
assume that
A4: O.x = f and
A5: O.y = g;
arity (O.x1) = arity (O.y1) by A3;
then
A6: dom g = (arity (O.x1))-tuples_on (B.y1) by A5,MARGREL1:22;
let n,m be Nat;
let X,Y be non empty set;
assume that
A7: dom f = n-tuples_on X and
A8: dom g = m-tuples_on Y;
dom f = (arity (O.x1))-tuples_on (B.x1) by A4,MARGREL1:22;
then
A9: n = arity (O.x1) by A7,FINSEQ_2:110;
set p = the Element of n-tuples_on X;
set q = the Element of 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 that
A10: f = o1 and
A11: g = o2;
A12: arity o2 = len q by A8,A11,MARGREL1:def 25
.= m by CARD_1:def 7;
arity o1 = len p by A7,A10,MARGREL1:def 25
.= n by CARD_1:def 7;
hence thesis by A8,A6,A9,A12,FINSEQ_2:110;
end;
definition
let F be Function-yielding Function, f be Function;
func F..f -> Function means
:Def17:
dom it = dom F & for x be set st x in dom F holds it.x = (F.x).(f.x);
existence
proof
set I = dom F;
defpred P[object,object] means $2 = (F.$1).(f.$1);
A1: for i be object st i in I ex y be object st P[i,y];
consider F be Function such that
A2: dom F = I & for i be object st i in I holds P[i,F.i] from CLASSES1:
sch 1( A1);
take F;
thus thesis by A2;
end;
uniqueness
proof
let m,n be Function;
assume that
A3: dom m = dom F and
A4: for x be set st x in dom F holds m.x = (F.x).(f.x) and
A5: dom n = dom F and
A6: for x be set st x in dom F holds n.x = (F.x).(f.x);
for x be object st x in dom m holds m.x = n.x
proof
let x be object;
consider g be set such that
A7: g = F.x;
reconsider g as Function by A7;
assume
A8: x in dom m;
then m.x = g.(f.x) by A3,A4,A7;
hence thesis by A3,A6,A8,A7;
end;
hence thesis by A3,A5;
end;
end;
registration
let I be set, f be (ManySortedFunction of I), x be ManySortedSet of I;
cluster f..x -> I-defined;
coherence
proof
dom(f..x) = dom f by Def17
.= I by PARTFUN1:def 2;
hence thesis by RELAT_1:def 18;
end;
end;
registration
let I be set, f be (ManySortedFunction of I), x be ManySortedSet of I;
cluster f..x -> total for I-defined Function;
coherence
proof
dom(f..x) = dom f by Def17
.= I by PARTFUN1:def 2;
hence thesis by PARTFUN1:def 2;
end;
end;
definition
let I be set, f be (ManySortedFunction of I), x be ManySortedSet of I;
redefine func f..x means
:Def18:
dom it = I & for i be set st i in I holds
for g be Function st g = f.i holds it.i = g.(x.i);
compatibility
proof
let M be Function;
hereby
assume
A1: M = f..x;
hence
A2: dom M = I by PARTFUN1:def 2;
dom M = dom f by A1,Def17;
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,A2,Def17;
end;
assume that
A3: dom M = I and
A4: for i be set st i in I holds for g be Function st g = f.i holds M.
i = g.(x.i);
A5: dom f = I by PARTFUN1:def 2;
then for i be set st i in dom f holds M.i = (f.i).(x.i) by A4;
hence thesis by A3,A5,Def17;
end;
end;
registration
let J be non empty set, B be non-empty ManySortedSet of J, p be FinSequence
of product B;
cluster uncurry p -> [:dom p, J:]-defined;
coherence
proof
now
set j = the Element of J;
dom B = J by PARTFUN1:def 2;
then B.j in rng B by FUNCT_1:def 3;
then reconsider S = union rng B as non empty set by XBOOLE_1:3
,ZFMISC_1:74;
rng p c= Funcs(J,S)
proof
let x be object;
A1: rng p c= product B by FINSEQ_1:def 4;
assume x in rng p;
then consider f be Function such that
A2: x = f and
A3: dom f = dom B and
A4: for y being object st y in dom B holds f.y in B.y by A1,CARD_3:def 5;
A5: rng f c= S
proof
let z be object;
assume z in rng f;
then consider y being object such that
A6: y in dom f and
A7: z = f.y by FUNCT_1:def 3;
B.y in rng B by A3,A6,FUNCT_1:def 3;
then
A8: B.y c= union rng B by ZFMISC_1:74;
z in B.y by A3,A4,A6,A7;
hence thesis by A8;
end;
dom B = J by PARTFUN1:def 2;
hence thesis by A2,A3,A5,FUNCT_2:def 2;
end;
then dom (uncurry p) = [:dom p,J:] by FUNCT_5:26;
hence thesis by RELAT_1:def 18;
end;
hence thesis;
end;
end;
registration
let J be non empty set, B be non-empty ManySortedSet of J, p be FinSequence
of product B;
cluster uncurry p -> total for [:dom p, J:]-defined Function;
coherence
proof
now
set j = the Element of J;
dom B = J by PARTFUN1:def 2;
then B.j in rng B by FUNCT_1:def 3;
then reconsider S = union rng B as non empty set by XBOOLE_1:3
,ZFMISC_1:74;
rng p c= Funcs(J,S)
proof
let x be object;
A1: rng p c= product B by FINSEQ_1:def 4;
assume x in rng p;
then consider f be Function such that
A2: x = f and
A3: dom f = dom B and
A4: for y being object st y in dom B holds f.y in B.y by A1,CARD_3:def 5;
A5: rng f c= S
proof
let z be object;
assume z in rng f;
then consider y being object such that
A6: y in dom f and
A7: z = f.y by FUNCT_1:def 3;
B.y in rng B by A3,A6,FUNCT_1:def 3;
then
A8: B.y c= union rng B by ZFMISC_1:74;
z in B.y by A3,A4,A6,A7;
hence thesis by A8;
end;
dom B = J by PARTFUN1:def 2;
hence thesis by A2,A3,A5,FUNCT_2:def 2;
end;
then dom (uncurry p) = [:dom p,J:] by FUNCT_5:26;
hence thesis by PARTFUN1:def 2;
end;
hence thesis;
end;
end;
registration
let I,J be set, X be ManySortedSet of [:I,J:];
cluster ~X -> [:J,I:]-defined;
coherence
proof
dom X = [:I,J:] by PARTFUN1:def 2;
then dom ~X = [:J,I:] by FUNCT_4:46;
hence thesis by RELAT_1:def 18;
end;
end;
registration
let I,J be set, X be ManySortedSet of [:I,J:];
cluster ~X -> total for [:J,I:]-defined Function;
coherence
proof
dom X = [:I,J:] by PARTFUN1:def 2;
then dom ~X = [:J,I:] by FUNCT_4:46;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let X be set, Y be non empty set, f be ManySortedSet of [:X,Y:];
cluster curry f -> X-defined;
coherence
proof
set a = curry f;
dom f = [:X,Y:] & dom a = proj1 dom f by FUNCT_5:def 1,PARTFUN1:def 2;
then dom a = X by FUNCT_5:9;
hence thesis by RELAT_1:def 18;
end;
end;
registration
let X be set, Y be non empty set, f be ManySortedSet of [:X,Y:];
cluster curry f -> total for X-defined Function;
coherence
proof
set a = curry f;
dom f = [:X,Y:] & dom a = proj1 dom f by FUNCT_5:def 1,PARTFUN1:def 2;
then dom a = X by FUNCT_5:9;
hence thesis by PARTFUN1:def 2;
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
:Def19:
for j be Element of J holds it = arity (O .j);
existence
proof
set i = the Element of J;
take arity (O.i);
let j be Element of J;
thus thesis by Th11;
end;
uniqueness
proof
set j = the Element of J;
let n,m be Nat;
assume that
A1: for j be Element of J holds n = arity (O.j) and
A2: for j be Element of J holds m = arity (O.j);
n = arity (O.j) by A1;
hence thesis by A2;
end;
end;
definition
::$CD
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..(
EmptyMS J) ) & ( 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[object,object] means
for p being Element of pr* st p = $1 holds ( dom
p = {} implies $2 = O..(EmptyMS J) ) & ( 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: for x being object st x in ct ex y being object st y in pr & P[x,y]
proof
let x be object;
assume x in ct;
then consider w be Element of pr* such that
A2: x = w and
A3: len w = ca;
now
per cases;
case
A4: dom w = {};
A5: for z being object st z in dom B holds (O..(EmptyMS J)).z in B.z
proof
let z be object;
assume z in dom B;
then reconsider j = z as Element of J by PARTFUN1:def 2;
A6: rng (O.j) c= B.j by RELAT_1:def 19;
w = {} by A4;
then arity (O.j) = 0 by A3,Def19;
then dom (O.j) = 0-tuples_on (B.j) by MARGREL1:22
.= {<*>(B.j)} by FINSEQ_2:94;
then {}(B.j) in dom (O.j) by TARSKI:def 1;
then
A7: (O.j).({}(B.j)) in rng (O.j) by FUNCT_1:def 3;
(O..(EmptyMS J)).z = (O.j).((EmptyMS J).j) by Def18
.= (O.j).({}(B.j));
hence thesis by A7,A6;
end;
take y = O..(EmptyMS J);
dom (O..(EmptyMS J)) = J by PARTFUN1:def 2
.= dom B by PARTFUN1:def 2;
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..(EmptyMS J)) & (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 A2,A4;
end;
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);
A8: for z being object st z in dom B holds (O..(curry p)).z in B.z
proof
let z be object;
assume z in dom B;
then reconsider j = z as Element of J by PARTFUN1:def 2;
A9: dom p = [:J,Z:] by PARTFUN1:def 2;
then proj1 dom p = J by FUNCT_5:9;
then consider g be Function such that
A10: (curry p).j = g and
A11: dom g = proj2 (dom p /\ [:{j},proj2 dom p:]) and
A12: for y st y in dom g holds g.y = p.(j,y) by FUNCT_5:def 1;
proj2 dom p = Z by A9,FUNCT_5:9;
then
A13: dom g = proj2 [:J /\ {j},Z /\ Z:] by A9,A11,ZFMISC_1:100
.= proj2 [:{j},Z:] by ZFMISC_1:46
.= dom w by FUNCT_5:9
.= 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 be object;
assume y in rng g;
then consider x being object such that
A14: x in dom g and
A15: g.x = y by FUNCT_1:def 3;
dom (uncurry w) = [:dom w,J:] & dom g = dom w by A13,
FINSEQ_1:def 3,PARTFUN1:def 2;
then
A16: [x,j] in dom (uncurry w) by A14,ZFMISC_1:87;
then consider a be object,f be Function, b be object such that
A17: [x,j] = [a,b] and
A18: a in dom w and
A19: f = w.a and
A20: b in dom f by FUNCT_5:def 2;
y = (~uncurry w).(j,x) by A12,A14,A15;
then
A21: y = (uncurry w).(x,j) by A16,FUNCT_4:def 2;
[a,b]`1 = a & [a,b]`2 = j by A17;
then
A22: y = f.j by A16,A21,A17,A19,FUNCT_5:def 2;
A23: j = b by A17,XTUPLE_0:1;
A24: rng w c= pr & w.a in rng w by A18,FINSEQ_1:def 4,FUNCT_1:def 3;
then dom f = dom B by A19,CARD_3:9;
hence thesis by A19,A20,A23,A24,A22,CARD_3:9;
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;
arity (O.j) = ca by Def19;
then
A25: dom (O.j) = ca-tuples_on (B.j) by MARGREL1:22
.= {s where s is Element of (B.j)* : len s = ca};
len g = len w by A13,FINSEQ_1:def 3;
then g in dom (O.j) by A3,A25;
then
A26: (O.j).g in rng (O.j) by FUNCT_1:def 3;
(O..(curry p)).z = (O.j).((curry p).j) & rng (O.j) c= B.j by Def18,
RELAT_1:def 19;
hence thesis by A10,A26;
end;
dom (O..(curry p)) = J by PARTFUN1:def 2
.= dom B by PARTFUN1:def 2;
hence y in pr by A8,CARD_3:def 5;
let l be Element of pr*;
assume l = x;
hence
(dom l = {} implies y = O..(EmptyMS J)) & (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 A2;
end;
end;
hence thesis;
end;
consider f being Function such that
A27: dom f = ct & rng f c= pr &
for x being object st x in ct holds P[x,f.x] from
FUNCT_1:sch 6(A1);
ct in the set of all n-tuples_on pr where n is Nat;
then
A28: ct c= union the set of all m-tuples_on pr where m is Nat by ZFMISC_1:74;
then dom f c= pr* by A27,FINSEQ_2:108;
then reconsider f as PartFunc of pr*,pr by A27,RELSET_1:4;
A29: f is homogeneous
proof
let x,y be FinSequence;
assume
A30: x in dom f & y in dom f;
then reconsider x1 = x, y1 = y as Element of pr* by A27,A28,FINSEQ_2:108;
( 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 A27,A30;
hence thesis;
end;
f is quasi_total
proof
let x,y be FinSequence of pr;
assume that
A31: len x = len y and
A32: 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 A27,A32;
then y1 in aa by A31;
hence thesis by A27;
end;
then reconsider
f as homogeneous quasi_total non empty PartFunc of pr*,pr by A27,A29;
take f;
thus dom f = ct by A27;
let p be Element of pr*;
assume p in dom f;
hence thesis by A27;
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
A33: dom f = ca-tuples_on pr and
A34: for p being Element of pr* st p in dom f holds (dom p = {}
implies f.p = O..(EmptyMS J) ) & (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
A35: dom g = ca-tuples_on pr and
A36: for p being Element of pr* st p in dom g holds (dom p = {}
implies g.p = O..(EmptyMS J) ) & (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 being object st x in ca-tuples_on pr holds f.x = g.x
proof
let x be object;
assume
A37: x in ca-tuples_on pr;
then consider s be Element of pr* such that
A38: x = s and
len s = ca;
per cases;
suppose
A39: dom s = {};
then f.s = O..(EmptyMS J) by A33,A34,A37,A38;
hence thesis by A35,A36,A37,A38,A39;
end;
suppose
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) by A33,A34,A37,A38;
hence thesis by A35,A36,A37,A38;
end;
end;
hence thesis by A33,A35;
end;
end;
definition
let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet
of J, n be Nat;
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[object,object] 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 being object st x in J ex y being object st P[x,y]
proof
let x be object;
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 4;
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
FUNCT_1:def 3;
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 being object st x in J holds P[x,f.x] from CLASSES1:sch 1(A2
);
reconsider f as ManySortedSet of J by A4,PARTFUN1:def 2,RELAT_1:def 18;
for x being object st x in dom f holds f.x is Function
proof
let x be object;
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 4;
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
FUNCT_1:def 3;
f.x = o by A4;
hence thesis;
end;
then reconsider f as ManySortedFunction of J by FUNCOP_1:def 6;
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 4;
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
FUNCT_1:def 3;
( ex R being 1-sorted st R = A.j & (Carrier A).j = the carrier of R
)& f.j = o by A4,Def13;
hence thesis;
end;
then reconsider f as ManySortedOperation of (Carrier A) by Def15;
for i,j be Element of J holds arity (f.i) = arity (f.j)
proof
let i,j be Element of J;
A5: n in dom (signature (A.j)) by A1,Def14;
then
A6: 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 4;
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
FUNCT_1:def 3;
A7: (signature A.j).n = arity (o) by A5,UNIALG_1:def 4;
dom A = J by PARTFUN1:def 2;
then
A8: signature A.i = signature A.j by Def12;
then n in Seg len (the charact of(A.i)) by A6,UNIALG_1:def 4;
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
FUNCT_1:def 3;
arity (f.j) = arity o & f.i = o1 by A4;
hence thesis by A8,A5,A7,UNIALG_1:def 4;
end;
then reconsider f as equal-arity ManySortedOperation of (Carrier A) by Th11
;
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 that
A9: 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 and
A10: 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 being object st x in J holds O1.x = O2.x
proof
let x be object;
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 4;
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
FUNCT_1:def 3;
O1.x1 = o by A9;
hence thesis by A10;
end;
hence thesis;
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
:Def22:
len
it = len (ComSign A) & for n st n in dom it holds it.n = [[: ProdOp(A,n) :]];
existence
proof
set f = ComSign A;
defpred P[Nat,set] means $2 = [[: ProdOp(A,$1) :]];
A1: for k being Nat 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 be Nat;
assume k in Seg len f;
reconsider a = [[: ProdOp(A,k) :]] as Element of PFuncs((product Carrier
A)*,product Carrier A) by PARTFUN1:45;
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 being Nat st k in Seg len f holds P[k,p.
k] from FINSEQ_1:sch 5(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 that
A3: len x = len (ComSign A) and
A4: for n st n in dom x holds x.n = [[: ProdOp(A, n) :]] and
A5: len y = len (ComSign A) and
A6: for n st n in dom y holds y.n = [[: ProdOp(A,n) :]];
A7: dom x = Seg len (ComSign A) by A3,FINSEQ_1:def 3;
now
let n be Nat;
assume n in dom x;
then n in dom y & x.n = [[: ProdOp(A,n) :]] by A4,A5,A7,FINSEQ_1:def 3;
hence x.n = y.n by A6;
end;
hence thesis by A3,A5,FINSEQ_2:9;
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 j = the Element of J;
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 that
A1: n in dom (the charact of ua) and
A2: (the charact of ua).n = h;
(the charact of ua).n = [[: ProdOp(A,n) :]] by A1,Def22;
hence thesis by A2;
end;
then
A3: the charact of(ua) is quasi_total;
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 that
A4: n in dom (the charact of ua) and
A5: (the charact of ua).n = h;
(the charact of ua).n = [[: ProdOp(A,n) :]] by A4,Def22;
hence thesis by A5;
end;
then
A6: the charact of(ua) is homogeneous;
for n be object st n in dom (the charact of ua) holds (the charact of ua
).n is non empty
proof
let n be object;
assume
A7: n in dom (the charact of ua);
then reconsider n9 = n as Element of NAT;
(the charact of ua).n = [[: ProdOp(A,n9) :]] by A7,Def22;
hence thesis;
end;
then
A8: the charact of(ua) is non-empty;
len the charact of(ua) = len ComSign A by Def22
.= len(signature A.j) by Def14
.= len the charact of(A.j) by UNIALG_1:def 4;
then the charact of(ua) <> {};
hence thesis by A3,A6,A8,UNIALG_1:def 1,def 2,def 3;
end;
end;