:: Product of Family of Universal Algebras
:: by Beata Madras
::
:: Received October 12, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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_4, FUNCT_5, PRALG_1, AFINSQ_1, ORDINAL4, ARYTM_3,
XXREAL_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, FUNCT_2,
BINOP_1, FUNCOP_1, ENUMSET1, MCART_1, DOMAIN_1, PARTFUN1, FINSEQ_2,
FUNCT_4, FUNCT_5, CARD_3, AFINSQ_1, 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, AFINSQ_1, FINSEQ_1,
XCMPLX_0, NAT_1, XXREAL_0;
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, AFINSQ_1, MEMBERED, XCMPLX_0, XXREAL_0, XREAL_0;
requirements NUMERALS, 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, ENUMSET1, AFINSQ_1;
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,h1;
redefine func pr1 h1 -> FinSequence of A means :: redefines pr1 (MCART_1, definition)
: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 :: redefines pr2 (MCART_1, definition)
: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
;
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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
hence thesis by A7,FINSEQ_2:9;
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:];
len the charact of(U4) = len signature(U2) by UNIALG_1:def 4,A3;
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;
len the charact of(U1) = len signature(U3) by UNIALG_1:def 4,A14;
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;
len the charact of(U1) = len signature(U2) by UNIALG_1:def 4,A5;
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,FUNCT_1:def 9;
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 Relation;
attr IT is 1-sorted-yielding means :Def11:
for x st x in rng IT holds x is 1-sorted;
end;
definition
let IT be Function;
redefine attr IT is 1-sorted-yielding means :Def11a: :: redefines 1-sorted-yielding (PRALG_1, definition)
for x st x in dom IT holds IT.x is 1-sorted;
compatibility
proof
thus IT is 1-sorted-yielding implies
for x st x in dom IT holds IT.x is 1-sorted by FUNCT_1:3;
assume
A2: for x st x in dom IT holds IT.x is 1-sorted;
for x st x in rng IT holds x is 1-sorted
proof
let x;
assume x in rng IT; then
consider xx being object such that
A3: xx in dom IT & x = IT.xx by FUNCT_1:def 3;
thus thesis by A2,A3;
end;
hence thesis;
end;
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;
reconsider f as ManySortedSet of I;
take f;
thus thesis by FUNCOP_1:7;
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;
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 A2,FUNCOP_1:7;
hence thesis by A3,A4,FUNCOP_1:7;
end;
hence f is equal-signature;
thus thesis by FUNCOP_1:7;
end;
end;
definition
let A be 1-sorted-yielding non empty Function,
j be Element of dom A;
redefine func A.j -> 1-sorted; :: redefines . (FUNCT_1, definition)
coherence by Def11a;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
dom A = J by PARTFUN1:def 2;
hence thesis by Def11a;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
dom A = J by PARTFUN1:def 2;
hence thesis by Def10;
end;
end;
definition
let A be 1-sorted-yielding Function;
func Carrier A -> Function means :Def13:
dom it = dom A &
for j be set st j in dom A
ex R being 1-sorted st R = A.j & it.j = the carrier of R;
existence
proof
set J = dom A;
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;
ex j being object st P[i,j]
proof
reconsider R = A.i9 as 1-sorted by Def11a;
take j = the carrier of R;
thus thesis;
end;
hence thesis;
end;
consider M being Function such that
A4: dom M = J &
for i being object st i in J holds P[i,M.i] from CLASSES1:sch 1(A1);
take M;
thus thesis by A4;
end;
uniqueness
proof
let X,Y be Function;
assume
A5: dom X = dom A & (for j be set st j in dom A
ex R being 1-sorted st R = A.j & X.j = the carrier of R) &
dom Y = dom A &
for j be set st j in dom A
ex R being 1-sorted st R = A.j & Y.j = the carrier of R;
for i be object st i in dom A holds X.i = Y.i
proof
let i be object;
assume i in dom A;
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 by A5;
end;
end;
definition
let J be set, A be 1-sorted-yielding ManySortedSet of J;
redefine func Carrier A -> ManySortedSet of J means :: redefines Carrier (PRALG_1, definition)
for j be set st j in J
ex R being 1-sorted st R = A.j & it.j = the carrier of R;
compatibility
proof
let f be ManySortedSet of J;
hereby assume
A1: f = Carrier A; then
A3: dom f = dom A by Def13;
A4: J = dom f by PARTFUN1:def 2;
let j be set;
assume j in J;
hence ex R being 1-sorted st R = A.j & f.j = the carrier of R
by A1,Def13,A4,A3;
end;
assume
B1: for j be set st j in J
ex R being 1-sorted st R = A.j & f.j = the carrier of R;
B0: dom Carrier A = dom A by Def13 .= J by PARTFUN1:def 2;
B4: J = dom f by PARTFUN1:def 2;
for j being set st j in J holds f.j = (Carrier A).j
proof
let j be set;
assume
B3: j in J; then
consider R being 1-sorted such that
B2: R = A.j & f.j = the carrier of R by B1;
J = dom A by PARTFUN1:def 2; then
ex R1 being 1-sorted st
R1 = A.j & (Carrier A).j = the carrier of R1 by Def13,B3;
hence thesis by B2;
end;
hence thesis by B0,B4;
end;
coherence
proof
A1: dom A = J by PARTFUN1:def 2;
dom Carrier A = dom A by Def13;
hence thesis by A1,RELAT_1:def 18,PARTFUN1:def 2;
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;
A0: dom A = J by PARTFUN1:def 2;
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,A0;
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 :: redefines . (FUNCT_1, definition)
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;
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 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;
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 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 /\ dom f &
for x be set st x in dom it holds it.x = (F.x).(f.x);
existence
proof
set I = dom F /\ 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 Ff be Function such that
A2: dom Ff = I & for i be object st i in I holds P[i,Ff.i]
from CLASSES1:sch 1(A1);
take Ff;
thus thesis by A2;
end;
uniqueness
proof
let m,n be Function;
assume that
A3: dom m = dom F /\ dom f and
A4: for x be set st x in dom m holds m.x = (F.x).(f.x) and
A5: dom n = dom F /\ dom f and
A6: for x be set st x in dom n 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
A9: m.x = g.(f.x) by A4,A7;
x in dom n by A3,A5,A8;
hence thesis by A6,A7,A9;
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 /\ dom x by Def17
.= I /\ dom x by PARTFUN1:def 2
.= I /\ 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 /\ dom x by Def17
.= I /\ dom x by PARTFUN1:def 2
.= I /\ 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 :: redefines .. (PRALG_1, definition)
: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;
thus 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 A6: for i be set st i in dom f holds M.i = (f.i).(x.i) by A4;
dom M = I /\ I by A3
.= I /\ dom x by PARTFUN1:def 2
.= dom f /\ dom x by PARTFUN1:def 2;
hence thesis by A3,A5,A6,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
B.y c= union rng B by ZFMISC_1:74;
hence thesis by A3,A4,A6,A7;
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
B.y c= union rng B by ZFMISC_1:74;
hence thesis by A3,A4,A6,A7;
end;
dom B = J by PARTFUN1:def 2;
hence thesis by A2,A3,A5,FUNCT_2:def 2;
end;
hence thesis by PARTFUN1:def 2,FUNCT_5:26;
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;
hence thesis by PARTFUN1:def 2,FUNCT_4:46;
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
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;
AA: J = dom A by PARTFUN1:def 2;
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,AA;
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 by FUNCT_1:def 9;
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;
begin :: Addenda, SK 14.11.2024
registration
let X be set, S be 1-sorted;
cluster X --> S -> 1-sorted-yielding;
coherence
proof
for x being object st x in rng (X --> S) holds x is 1-sorted
proof
let x be object;
per cases;
suppose A1: X <> {};
assume x in rng (X --> S);
then x in {S} by A1,FUNCOP_1:8;
hence thesis by TARSKI:def 1;
end;
suppose X = {};
hence thesis;
end;
end;
hence thesis;
end;
end;
registration
let x be object, S be 1-sorted;
cluster x .--> S -> 1-sorted-yielding;
coherence;
cluster {[x,S]} -> 1-sorted-yielding;
coherence
proof
x .--> S = {[x,S]} by FUNCT_4:82;
hence thesis;
end;
end;
registration
let S1 be 1-sorted;
cluster <* S1 *> -> 1-sorted-yielding;
coherence
proof
for x being object st x in rng <* S1 *> holds x is 1-sorted
proof
let x be object;
assume x in rng <* S1 *>;
then x in { S1 } by FINSEQ_1:38;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
cluster <% S1 %> -> 1-sorted-yielding;
coherence
proof
for x being object st x in rng <% S1 %> holds x is 1-sorted
proof
let x be object;
assume x in rng <% S1 %>;
then x in { S1 } by AFINSQ_1:33;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
let S2 be 1-sorted;
cluster <* S1, S2 *> -> 1-sorted-yielding;
coherence
proof
for x being object st x in rng <* S1, S2 *> holds x is 1-sorted
proof
let x be object;
assume x in rng <* S1, S2 *>;
then x in { S1, S2 } by FINSEQ_2:127;
hence thesis by TARSKI:def 2;
end;
hence thesis;
end;
cluster <% S1, S2 %> -> 1-sorted-yielding;
coherence
proof
for x being object st x in rng <% S1, S2 %> holds x is 1-sorted
proof
let x be object;
assume x in rng <% S1, S2 %>;
then x in { S1, S2 } by AFINSQ_1:98;
hence thesis by TARSKI:def 2;
end;
hence thesis;
end;
let S3 be 1-sorted;
cluster <* S1, S2, S3 *> -> 1-sorted-yielding;
coherence
proof
for x being object st x in rng <* S1, S2, S3 *> holds x is 1-sorted
proof
let x be object;
assume x in rng <* S1, S2, S3 *>;
then x in { S1, S2, S3 } by FINSEQ_2:128;
hence thesis by ENUMSET1:def 1;
end;
hence thesis;
end;
cluster <% S1, S2, S3 %> -> 1-sorted-yielding;
coherence
proof
for x being object st x in rng <% S1, S2, S3 %> holds x is 1-sorted
proof
let x be object;
assume x in rng <% S1, S2, S3 %>;
then x in { S1, S2, S3 } by AFINSQ_1:99;
hence thesis by ENUMSET1:def 1;
end;
hence thesis;
end;
end;
registration
cluster FinSequence-like 1-sorted-yielding for Function;
existence
proof
take <* the 1-sorted *>;
thus thesis;
end;
end;
registration
let f,g be 1-sorted-yielding Function;
cluster f+*g -> 1-sorted-yielding;
coherence
proof
for x being object st x in rng(f+*g) holds x is 1-sorted
proof
let x be object;
assume x in rng(f+*g);
then x in rng f \/ rng g by TARSKI:def 3, FUNCT_4:17;
then per cases by XBOOLE_0:def 3;
suppose x in rng f;
hence thesis by Def11;
end;
suppose x in rng g;
hence thesis by Def11;
end;
end;
hence thesis;
end;
end;
theorem
for f,g be 1-sorted-yielding Function holds
f tolerates g implies Carrier f tolerates Carrier g
proof
let f,g be 1-sorted-yielding Function;
assume A1: f tolerates g;
now
let x be object;
assume x in dom Carrier f /\ dom Carrier g;
then x in dom Carrier f /\ dom g by Def13;
then A2: x in dom f /\ dom g & x is set by Def13;
then A3: x in dom f & x in dom g by XBOOLE_0:def 4;
A4: f.x = g.x by A1, A2, PARTFUN1:def 4;
consider R1 being 1-sorted such that
A5: R1 = f.x & (Carrier f).x = the carrier of R1 by A3, Def13;
consider R2 being 1-sorted such that
A6: R2 = g.x & (Carrier g).x = the carrier of R2 by A3, Def13;
thus (Carrier f).x = (Carrier g).x by A4, A5, A6;
end;
hence thesis by PARTFUN1:def 4;
end;
theorem
for f,g be 1-sorted-yielding Function holds
Carrier(f+*g) = Carrier f +* Carrier g
proof
let f,g be 1-sorted-yielding Function;
A1: dom Carrier(f+*g) = dom(f+*g) by Def13
.= dom f \/ dom g by FUNCT_4:def 1;
then A2: dom Carrier(f+*g) = dom Carrier f \/ dom g by Def13
.= dom Carrier f \/ dom Carrier g by Def13
.= dom(Carrier f +* Carrier g) by FUNCT_4:def 1;
now
let x be object;
assume x in dom Carrier(f+*g);
then A3: x in dom f \/ dom g & x is set by A1;
then x in dom(f+*g) by FUNCT_4:def 1;
then consider R being 1-sorted such that
A4: R=(f+*g).x & (Carrier(f+*g)).x = the carrier of R by Def13;
per cases;
suppose A5: x in dom g;
then consider R9 being 1-sorted such that
A6: R9 = g.x & (Carrier g).x = the carrier of R9 by Def13;
R = R9 & x in dom Carrier g by A4, A5, A6, FUNCT_4:13, Def13;
hence (Carrier(f+*g)).x = (Carrier f +* Carrier g).x
by A4, A6, FUNCT_4:13;
end;
suppose A8: not x in dom g; then
A9: not x in dom Carrier g & x in dom f
by A3, XBOOLE_0:def 3, Def13;
then consider R9 being 1-sorted such that
A10: R9 = f.x & (Carrier f).x = the carrier of R9 by Def13;
R = R9 by A4, A8, A10, FUNCT_4:11;
hence (Carrier(f+*g)).x = (Carrier f +* Carrier g).x
by A4, A9, A10, FUNCT_4:11;
end;
end;
hence thesis by A2;
end;
registration
let p be 1-sorted-yielding FinSequence;
cluster Carrier p -> FinSequence-like;
coherence
proof
consider n being Nat such that
A1: dom p = Seg n by FINSEQ_1:def 2;
dom Carrier p = dom p by Def13;
hence thesis by A1, FINSEQ_1:def 2;
end;
let q be 1-sorted-yielding FinSequence;
cluster p^q -> 1-sorted-yielding;
coherence
proof
for x being object st x in rng(p^q) holds x is 1-sorted
proof
let x be object;
assume x in rng(p^q);
then x in rng p \/ rng q by FINSEQ_1:31;
then per cases by XBOOLE_0:def 3;
suppose x in rng p;
hence thesis by Def11;
end;
suppose x in rng q;
hence thesis by Def11;
end;
end;
hence thesis;
end;
end;
theorem Th13:
for p being 1-sorted-yielding FinSequence holds len Carrier p = len p
proof
let p be 1-sorted-yielding FinSequence;
dom Carrier p = dom p by Def13;
hence thesis by FINSEQ_3:29;
end;
theorem Th14:
for p,q being 1-sorted-yielding FinSequence holds
Carrier(p^q) = Carrier p ^ Carrier q
proof
let p,q be 1-sorted-yielding FinSequence;
A1: len Carrier(p^q) = len(p^q) by Th13
.= len p + len q by FINSEQ_1:22
.= len Carrier p + len q by Th13
.= len Carrier p + len Carrier q by Th13
.= len(Carrier p ^ Carrier q) by FINSEQ_1:22;
now
let k be Nat;
assume 1 <= k <= len Carrier(p^q);
then k in dom Carrier(p^q) by FINSEQ_3:25;
then A3: k in dom(p^q) by Def13;
then consider R being 1-sorted such that
A4: R=(p^q).k & (Carrier(p^q)).k = the carrier of R by Def13;
per cases by A3, FINSEQ_1:25;
suppose A5: k in dom p;
then consider R9 being 1-sorted such that
A6: R9=p.k & (Carrier p).k = the carrier of R9 by Def13;
A7: k in dom Carrier p by A5, Def13;
R = R9 by A4, A5, A6, FINSEQ_1:def 7;
hence (Carrier(p^q)).k = (Carrier p ^ Carrier q).k
by A4, A6, A7, FINSEQ_1:def 7;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A8: n in dom q & k = len p + n;
consider R9 being 1-sorted such that
A9: R9=q.n & (Carrier q).n = the carrier of R9 by A8, Def13;
A10: n in dom Carrier q & k = len Carrier p + n
by A8, Th13, Def13;
R = R9 by A4, A8, A9, FINSEQ_1:def 7;
hence (Carrier(p^q)).k = (Carrier p ^ Carrier q).k
by A4, A9, A10, FINSEQ_1:def 7;
end;
end;
hence thesis by A1, FINSEQ_1:def 18;
end;
theorem Th15:
for X being set, S being 1-sorted holds
Carrier(X --> S) = X --> the carrier of S
proof
let X be set, S be 1-sorted;
A1: dom Carrier(X --> S) = dom(X --> S) by Def13
.= dom(X --> the carrier of S);
now
let x be object;
assume x in dom Carrier(X --> S); then
A2: x in dom(X --> S) by Def13;
then consider R being 1-sorted such that
A4: R = (X-->S).x & (Carrier(X-->S)).x = the carrier of R
by Def13;
thus Carrier(X --> S).x = the carrier of S by A2, A4, FUNCOP_1:7
.= (X --> the carrier of S).x by A2, FUNCOP_1:7;
end;
hence thesis by A1;
end;
theorem Th16:
for S being 1-sorted
holds Carrier <* S *> = <* the carrier of S *>
proof
let S be 1-sorted;
thus Carrier <* S *> = Carrier {[1,S]} by FINSEQ_1:def 5
.= Carrier(1 .--> S) by FUNCT_4:82
.= Carrier({1} --> S)
.= {1} --> the carrier of S by Th15
.= 1 .--> the carrier of S
.= {[1,the carrier of S]} by FUNCT_4:82
.= <* the carrier of S *> by FINSEQ_1:def 5;
end;
theorem Th17:
for S1, S2 being 1-sorted holds
Carrier <* S1, S2 *> = <* the carrier of S1, the carrier of S2 *>
proof
let S1, S2 be 1-sorted;
thus Carrier <* S1, S2 *> = Carrier(<*S1*>^<*S2*>) by FINSEQ_1:def 9
.= Carrier<*S1*> ^ Carrier<*S2*> by Th14
.= <*the carrier of S1*> ^ Carrier<*S2*> by Th16
.= <* the carrier of S1 *> ^ <* the carrier of S2 *> by Th16
.= <* the carrier of S1, the carrier of S2 *> by FINSEQ_1:def 9;
end;
theorem
for S1, S2, S3 being 1-sorted holds Carrier <* S1, S2, S3 *>
= <* the carrier of S1, the carrier of S2, the carrier of S3 *>
proof
let S1, S2, S3 be 1-sorted;
set C = <* the carrier of S1, the carrier of S2 *>;
thus Carrier <* S1, S2, S3 *> = Carrier(<* S1, S2 *>^<*S3*>) by FINSEQ_1:43
.= Carrier<*S1,S2*> ^ Carrier<*S3*> by Th14
.= C ^ Carrier<*S3*> by Th17
.= C ^ <*the carrier of S3*> by Th16
.= <* the carrier of S1, the carrier of S2, the carrier of S3 *>
by FINSEQ_1:43;
end;