:: Products of Many Sorted Algebras
:: by Beata Madras
::
:: Received April 25, 1994
:: Copyright (c) 1994-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, MSUALG_1, CARD_3, FUNCT_1, SUBSET_1, PBOOLE, RELAT_1,
FUNCT_6, TARSKI, FUNCOP_1, FINSEQ_4, FUNCT_5, ZFMISC_1, PRALG_1, MCART_1,
COMPLEX1, STRUCT_0, MARGREL1, RLVECT_2, FUNCT_2, PRALG_2, PARTFUN1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, BINOP_1, XTUPLE_0, MCART_1, STRUCT_0, FUNCOP_1, FINSEQ_2,
FUNCT_5, FUNCT_6, CARD_3, PBOOLE, PRALG_1, MSUALG_1;
constructors BINOP_1, FUNCT_6, PRALG_1, MSUALG_1, RELSET_1, FUNCT_5, XTUPLE_0,
SETFAM_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, CARD_3, PBOOLE, STRUCT_0,
MSUALG_1, RELSET_1, FINSEQ_2, FINSEQ_1, XTUPLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, PBOOLE, FUNCOP_1, XBOOLE_0, FUNCT_2;
equalities PBOOLE, BINOP_1, FUNCT_6;
expansions TARSKI, PBOOLE;
theorems TARSKI, FUNCT_1, FINSEQ_1, PBOOLE, MSUALG_1, ZFMISC_1, CARD_3,
FUNCT_2, MCART_1, FUNCOP_1, FUNCT_6, FUNCT_5, RELAT_1, PRALG_1, XBOOLE_0,
PARTFUN1, FINSEQ_2;
schemes FUNCT_1, FUNCT_2, CLASSES1, TARSKI, PBOOLE;
begin
reserve I,J for set,i,j,x for object,
S for non empty ManySortedSign;
::
:: Preliminaries
::
registration
let X be with_common_domain functional non empty set;
cluster -> DOM X -defined for Element of X;
coherence
proof
let x be Element of X;
DOM X = dom x by CARD_3:108;
hence thesis by RELAT_1:def 18;
end;
end;
registration
let X be with_common_domain functional non empty set;
cluster -> total for Element of X;
coherence
proof
let x be Element of X;
DOM X = dom x by CARD_3:108;
hence thesis by PARTFUN1:def 2;
end;
end;
begin
:: Operations on Functions
definition
let F be Function;
func Commute F -> Function means :Def1:
(for x holds x in dom it iff
ex f being Function st f in dom F & x = commute f) &
for f being Function st f in dom it holds it.f = F.commute f;
existence
proof
defpred P[object,object] means
ex f being Function st $1 = f & $2 = commute f;
A1: for x,y1,y2 being object st P[x,y1] & P[x,y2] holds y1 = y2;
consider X being set such that
A2: for x being object holds x in X iff
ex y being object st y in dom F & P[y,x] from TARSKI:sch 1(A1);
defpred P[object,object] means
for f be Function st $1 = f holds $2 = F.commute
f;
A3: now
let x be object;
assume x in X;
then ex y being object st y in dom F &
ex f being Function st y = f & x = commute f by A2;
then reconsider f = x as Function;
reconsider y = F.commute f as object;
take y;
thus P[x,y];
end;
consider G being Function such that
A4: dom G = X and
A5: for x being object st x in X holds P[x,G.x] from CLASSES1:sch 1(A3);
take G;
hereby
let x;
hereby
assume x in dom G;
then consider y being object such that
A6: y in dom F and
A7: ex f being Function st y = f & x = commute f by A2,A4;
reconsider f = y as Function by A7;
take f;
thus f in dom F & x = commute f by A6,A7;
end;
thus (ex f being Function st f in dom F & x = commute f) implies x in
dom G by A2,A4;
end;
thus thesis by A4,A5;
end;
uniqueness
proof
let m,n be Function such that
A8: for x holds x in dom m iff ex f being Function st f in dom F & x
= commute f and
A9: for f being Function st f in dom m holds m.f = F.commute f and
A10: for x holds x in dom n iff ex f being Function st f in dom F & x
= commute f and
A11: for f being Function st f in dom n holds n.f = F.commute f;
now
let x be object;
x in dom m iff ex f being Function st f in dom F & x = commute f by A8;
hence x in dom m iff x in dom n by A10;
end;
then
A12: dom m = dom n by TARSKI:2;
now
let x be object;
assume
A13: x in dom m;
then consider g being Function such that
g in dom F and
A14: x = commute g by A10,A12;
thus m.x = F.commute commute g by A9,A13,A14
.= n.x by A11,A12,A13,A14;
end;
hence thesis by A12,FUNCT_1:2;
end;
end;
theorem
for F be Function st dom F = {{}} holds Commute F = F
proof
let F be Function;
assume
A1: dom F = {{}};
A2: dom (Commute F) = {{}}
proof
thus dom (Commute F) c= {{}}
proof
let x be object;
assume x in dom (Commute F);
then ex f be Function st f in dom F & x = commute f by Def1;
then x = {} by A1,FUNCT_6:58,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {{}};
then
A3: x = {} by TARSKI:def 1;
{} in dom F by A1,TARSKI:def 1;
hence thesis by A3,Def1,FUNCT_6:58;
end;
for x being object st x in {{}} holds (Commute F).x = F.x
proof
let x be object;
assume
A4: x in {{}};
then x = {} by TARSKI:def 1;
hence thesis by A2,A4,Def1,FUNCT_6:58;
end;
hence thesis by A1,A2,FUNCT_1:2;
end;
definition
let f be Function-yielding Function;
redefine func Frege f -> ManySortedFunction of product doms f means :Def2: :: redefines Frege (FUNCT_6, definition)
for g be Function st g in product doms f holds it.g = f..g;
coherence
proof
A1: dom Frege f = product doms f by FUNCT_6:def 7;
Frege f is Function-yielding
proof
let x be object;
assume
A2: x in dom Frege f;
then reconsider g = x as Function by A1;
ex h being Function st (Frege f).g = h & dom h = dom f &
for x st x in dom h holds h.x = (uncurry f).(x,g.x)
by A1,A2,FUNCT_6:def 7;
hence thesis;
end;
hence thesis by A1,PARTFUN1:def 2,RELAT_1:def 18;
end;
compatibility
proof
let F be ManySortedFunction of product doms f;
thus F = Frege f implies for g be Function st g in product doms f holds
F.g = f..g
proof
assume
A3: F = Frege f;
let g be Function;
assume
A4: g in product doms f;
then consider h being Function such that
A5: F.g = h and
A6: dom h = dom f and
A7: for x st x in dom h holds h.x = (uncurry f).(x,g.x) by A3,FUNCT_6:def 7;
consider gg being Function such that
a13: g = gg & dom gg = dom doms f &
for y being object st y in dom doms f holds gg.y in (doms f).y
by CARD_3:def 5,A4;
dom g = dom f by a13,FUNCT_6:def 2; then
A8: dom h = dom f /\ dom g by A6;
for x be set st x in dom h holds h.x = (f.x).(g.x)
proof
let x be set;
assume
A9: x in dom h; then
x in dom doms f by A6,FUNCT_6:def 2;
then g.x in (doms f).x by A4,CARD_3:9; then
A10: g.x in dom(f.x) by A9,A6,FUNCT_6:22;
thus h.x = f..(x,g.x) by A7,A9
.= (f.x).(g.x) by A9,A6,A10,FUNCT_5:38;
end;
hence thesis by A5,A8,PRALG_1:def 19;
end;
assume
A11: for g be Function st g in product doms f holds F.g = f..g;
A12: for g being Function st g in product doms f
ex h being Function st F.g = h & dom h = dom f &
for x being object st x in dom h holds h.x = (uncurry f).(x,g.x)
proof
let g be Function such that
A13: g in product doms f;
consider gg being Function such that
a13: g = gg & dom gg = dom doms f &
for y being object st y in dom doms f holds gg.y in (doms f).y
by CARD_3:def 5,A13;
a14: F.g = f..g by A11,A13; then
A14: dom(F.g) = dom f /\ dom g by PRALG_1:def 19;
take F.g;
thus F.g = F.g;
WW: dom g = dom f by a13,FUNCT_6:def 2;
hence dom(F.g) = dom f by A14;
let x be object;
assume
A15: x in dom (F.g);
then x in dom doms f by WW,A14,FUNCT_6:def 2;
then g.x in (doms f).x by A13,CARD_3:9; then
A16: g.x in dom(f.x) by A14,A15,FUNCT_6:22,WW;
thus (F.g).x = (f..g).x by A11,A13
.= (f.x).(g.x) by A15,PRALG_1:def 19,a14
.= (uncurry f).(x,g.x) by A14,A15,A16,FUNCT_5:38,WW;
end;
dom F = product doms f by PARTFUN1:def 2;
hence thesis by A12,FUNCT_6:def 7;
end;
end;
registration
let I;
let A,B be non-empty ManySortedSet of I;
cluster [|A,B|] -> non-empty;
coherence
proof
now
let i be object;
assume
A1: i in I;
then [|A,B|].i = [:A.i,B.i:] by PBOOLE:def 16;
hence [|A,B|].i is non empty by A1,ZFMISC_1:90;
end;
hence thesis;
end;
end;
theorem
for I be non empty set, J be set, A,B be ManySortedSet of I,
f be Function of J,I holds [|A,B|]*f = [|A*f,B*f|]
proof
let I be non empty set, J be set, A,B be ManySortedSet of I, f be Function
of J,I;
for i being object st i in J holds ([|A,B|]*f).i = ([|A*f,B*f|]).i
proof
A1: dom (B*f) = J by PARTFUN1:def 2;
let i be object;
A2: dom (A*f) = J by PARTFUN1:def 2;
assume
A3: i in J; then
A4: f.i in I by FUNCT_2:5;
dom ([|A,B|]*f) = J by PARTFUN1:def 2;
hence ([|A,B|]*f).i = [|A,B|].(f.i) by A3,FUNCT_1:12
.= [:A.(f.i),B.(f.i):] by A4,PBOOLE:def 16
.= [:(A*f).i,B.(f.i):] by A3,A2,FUNCT_1:12
.= [:(A*f).i,(B*f).i:] by A3,A1,FUNCT_1:12
.= [|A*f,B*f|].i by A3,PBOOLE:def 16;
end;
hence thesis;
end;
definition
let I be non empty set;
let A,B be non-empty ManySortedSet of I,
pj being Element of I*, rj being Element of I,
f be Function of A#.pj,A.rj, g be Function of B#.pj,B.rj;
func [[:f,g:]] -> Function of [|A,B|]#.pj,[|A,B|].rj means
for h be Function st h in [|A,B|]#.pj holds it.h = [f.(pr1 h),g.(pr2 h)];
existence
proof
defpred P[object,object] means
for h be Function st h = $1 holds $2 = [f.(pr1 h)
,g.(pr2 h)];
set Y = [|A,B|].rj, X = [|A,B|]#.pj;
A1: X = product ([|A,B|]*pj) by FINSEQ_2:def 5;
A2: for x be object st x in X ex y be object st y in Y & P[x,y]
proof
let x be object;
A3: rng pj c= I by FINSEQ_1:def 4;
assume x in X;
then consider h1 be Function such that
A4: h1 = x and
A5: dom h1 = dom ([|A,B|]*pj) and
A6: for z be object st z in dom ([|A,B|]*pj) holds h1.z in ([|A,B|]*pj)
.z by A1,CARD_3:def 5;
A7: dom [|A,B|] = I by PARTFUN1:def 2; then
A8: dom h1 = dom pj by A5,A3,RELAT_1:27; then
A9: dom (pr1 h1) = dom pj by MCART_1:def 12;
dom A = I by PARTFUN1:def 2; then
A10: dom (pr1 h1) = dom (A*pj) by A3,A9,RELAT_1:27;
for z be object st z in dom (A*pj) holds (pr1 h1).z in (A*pj).z
proof
let z be object;
assume
A11: z in dom (A*pj);
dom ([|A,B|]*pj) = dom pj by A7,A3,RELAT_1:27; then
A12: ([|A,B|]*pj).z = [|A,B|].(pj.z) by A9,A10,A11,FUNCT_1:12;
h1.z in ([|A,B|]*pj).z & pj.z in rng pj by A5,A6,A8,A9,A10,A11,
FUNCT_1:def 3;
then h1.z in [:A.(pj.z),B.(pj.z):] by A3,A12,PBOOLE:def 16;
then consider a,b be object such that
A13: a in A.(pj.z) and
b in B.(pj.z) and
A14: h1.z = [a,b] by ZFMISC_1:def 2;
(pr1 h1).z = (h1.z)`1 by A8,A9,A10,A11,MCART_1:def 12
.= a by A14;
hence thesis by A11,A13,FUNCT_1:12;
end;
then pr1 h1 in product (A*pj) by A10,CARD_3:9;
then pr1 h1 in A#.pj by FINSEQ_2:def 5;
then pr1 h1 in dom f by FUNCT_2:def 1;
then
A15: f.(pr1 h1) in rng f by FUNCT_1:3;
take y = [f.(pr1 h1),g.(pr2 h1)];
rng f c= A.rj & rng g c= B.rj by RELAT_1:def 19;
then
A16: [:rng f,rng g:] c= [:A.rj,B.rj:] by ZFMISC_1:96;
A17: dom (pr2 h1) = dom pj by A8,MCART_1:def 13;
A18: dom B = I by PARTFUN1:def 2;
then
A19: dom (pr2 h1) = dom (B*pj) by A3,A17,RELAT_1:27;
A20: for z be object st z in dom (B*pj) holds (pr2 h1).z in (B*pj).z
proof
let z be object;
assume
A21: z in dom (B*pj);
dom ([|A,B|]*pj) = dom pj by A7,A3,RELAT_1:27; then
A22: ([|A,B|]*pj).z = [|A,B|].(pj.z) by A17,A19,A21,FUNCT_1:12;
h1.z in ([|A,B|]*pj).z & pj.z in rng pj
by A5,A6,A8,A17,A19,A21,FUNCT_1:def 3;
then h1.z in [:A.(pj.z),B.(pj.z):] by A3,A22,PBOOLE:def 16;
then consider a,b be object such that
a in A.(pj.z) and
A23: b in B.(pj.z) and
A24: h1.z = [a,b] by ZFMISC_1:def 2;
(pr2 h1).z = (h1.z)`2 by A8,A17,A19,A21,MCART_1:def 13
.= b by A24;
hence thesis by A21,A23,FUNCT_1:12;
end;
dom (pr2 h1) = dom pj by A8,MCART_1:def 13;
then dom (pr2 h1) = dom (B*pj) by A18,A3,RELAT_1:27;
then pr2 h1 in product (B*pj) by A20,CARD_3:9;
then pr2 h1 in B#.pj by FINSEQ_2:def 5;
then pr2 h1 in dom g by FUNCT_2:def 1;
then g.(pr2 h1) in rng g by FUNCT_1:3;
then [f.(pr1 h1),g.(pr2 h1)] in [:rng f,rng g:] by A15,ZFMISC_1:87;
then [f.(pr1 h1),g.(pr2 h1)] in [:A.rj,B.rj:] by A16;
hence y in Y by PBOOLE:def 16;
let h be Function;
assume x = h;
hence thesis by A4;
end;
consider F being Function of X,Y such that
A25: for x be object st x in X holds P[x,F.x] from FUNCT_2:sch 1(A2);
take F;
thus thesis by A25;
end;
uniqueness
proof
let x,y be Function of [|A,B|]#.pj,[|A,B|].rj such that
A26: for h be Function st h in [|A,B|]#.pj holds x.h = [f.(pr1 h),g.(
pr2 h)] and
A27: for h be Function st h in [|A,B|]#.pj holds y.h = [f.(pr1 h),g.( pr2 h)];
let h be Element of [|A,B|]#.pj;
h in [|A,B|]#.pj;
then h in product ([|A,B|]*pj) by FINSEQ_2:def 5;
then consider h1 be Function such that
A28: h1 = h and
dom h1 = dom ([|A,B|]*pj) and
for z be object st z in dom ([|A,B|]*pj) holds h1.z in ([|A,B|]*pj).z by
CARD_3:def 5;
x.h1 = [f.(pr1 h1),g.(pr2 h1)] by A26,A28;
hence x.h = y.h by A27,A28;
end;
end;
definition
let I be non empty set,J;
let A,B be non-empty ManySortedSet of I, p be Function of J,I*, r be
Function of J,I, F be ManySortedFunction of A#*p,A*r, G be ManySortedFunction
of B#*p,B*r;
func [[:F,G:]] -> ManySortedFunction of [|A,B|]#*p,[|A,B|]*r means
for j st
j in J for pj being Element of I*, rj being Element of I st pj = p.j & rj = r.j
for f be Function of A#.pj,A.rj, g be Function of B#.pj,B.rj st f = F.j & g = G
.j holds it.j = [[:f,g:]];
existence
proof
defpred P[object,object] means
for pj being Element of I*, rj being Element of I
st pj = p.$1 & rj = r.$1 for f be Function of A#.pj,A.rj, g be Function of B#.
pj,B.rj st f = F.$1 & g = G.$1 holds $2 = [[:f,g:]];
A1: for j being object st j in J ex i being object st P[j,i]
proof
let j be object;
assume
A2: j in J;
then reconsider pj = p.j as Element of I* by FUNCT_2:5;
reconsider rj = r.j as Element of I by A2,FUNCT_2:5;
A3: j in dom r by A2,FUNCT_2:def 1;
then
A4: A.(r.j) = (A*r).j by FUNCT_1:13;
A5: B.(r.j) = (B*r).j by A3,FUNCT_1:13;
A6: j in dom p by A2,FUNCT_2:def 1;
then A#.(p.j) = (A#*p).j by FUNCT_1:13;
then reconsider f = F.j as Function of A#.pj,A.rj by A2,A4,PBOOLE:def 15;
B#.(p.j) = (B#*p).j by A6,FUNCT_1:13;
then reconsider g = G.j as Function of B#.pj,B.rj by A2,A5,PBOOLE:def 15;
take [[:f,g:]];
thus thesis;
end;
consider h being Function such that
A7: dom h = J &
for j being object st j in J holds P[j,h.j] from CLASSES1:sch 1(A1);
reconsider h as ManySortedSet of J by A7,PARTFUN1:def 2,RELAT_1:def 18;
for j being object st j in dom h holds h.j is Function
proof
let j be object;
assume
A8: j in dom h;
then reconsider pj = p.j as Element of I* by A7,FUNCT_2:5;
reconsider rj = r.j as Element of I by A7,A8,FUNCT_2:5;
A9: j in dom r by A7,A8,FUNCT_2:def 1;
then
A10: A.(r.j) = (A*r).j by FUNCT_1:13;
A11: B.(r.j) = (B*r).j by A9,FUNCT_1:13;
A12: j in dom p by A7,A8,FUNCT_2:def 1;
then A#.(p.j) = (A#*p).j by FUNCT_1:13;
then reconsider f = F.j as Function of A#.pj,A.rj by A7,A8,A10,
PBOOLE:def 15;
B#.(p.j) = (B#*p).j by A12,FUNCT_1:13;
then reconsider g = G.j as Function of B#.pj,B.rj
by A7,A8,A11,PBOOLE:def 15;
h.j = [[:f,g:]] by A7,A8;
hence thesis;
end;
then reconsider h as ManySortedFunction of J by FUNCOP_1:def 6;
for j st j in J holds h.j is Function of ([|A,B|]#*p).j,([|A,B|]*r).j
proof
let j;
assume
A13: j in J;
then reconsider pj = p.j as Element of I* by FUNCT_2:5;
reconsider rj = r.j as Element of I by A13,FUNCT_2:5;
A14: j in dom p by A13,FUNCT_2:def 1;
then
A15: ([|A,B|]#*p).j = [|A,B|]#.(p.j) by FUNCT_1:13;
A16: j in dom r by A13,FUNCT_2:def 1;
then
A17: A.(r.j) = (A*r).j by FUNCT_1:13;
A18: ([|A,B|]*r).j = [|A,B|].(r.j) by A16,FUNCT_1:13;
A19: B.(r.j) = (B*r).j by A16,FUNCT_1:13;
B#.(p.j) = (B#*p).j by A14,FUNCT_1:13;
then reconsider g = G.j as Function of B#.pj,B.rj by A13,A19,
PBOOLE:def 15;
A#.(p.j) = (A#*p).j by A14,FUNCT_1:13;
then reconsider f = F.j as Function of A#.pj,A.rj by A13,A17,
PBOOLE:def 15;
h.j = [[:f,g:]] by A7,A13;
hence thesis by A15,A18;
end;
then reconsider h as ManySortedFunction of [|A,B|]#*p,[|A,B|]*r by
PBOOLE:def 15;
take h;
thus thesis by A7;
end;
uniqueness
proof
let x,y be ManySortedFunction of [|A,B|]#*p,[|A,B|]*r;
assume that
A20: for j st j in J for pj being Element of I*, rj being Element of I
st pj = p.j & rj = r.j for f be Function of A#.pj,A.rj, g be Function of B#.pj,
B.rj st f = F.j & g = G.j holds x.j = [[:f,g:]] and
A21: for j st j in J for pj being Element of I*, rj being Element of I
st pj = p.j & rj = r.j for f be Function of A#.pj,A.rj, g be Function of B#.pj,
B.rj st f = F.j & g = G.j holds y.j = [[:f,g:]];
for j be object st j in J holds x.j = y.j
proof
let j be object;
assume
A22: j in J;
then reconsider pj = p.j as Element of I* by FUNCT_2:5;
reconsider rj = r.j as Element of I by A22,FUNCT_2:5;
A23: j in dom r by A22,FUNCT_2:def 1;
then
A24: A.(r.j) = (A*r).j by FUNCT_1:13;
A25: B.(r.j) = (B*r).j by A23,FUNCT_1:13;
A26: j in dom p by A22,FUNCT_2:def 1;
then A#.(p.j) = (A#*p).j by FUNCT_1:13;
then reconsider f = F.j as Function of A#.pj,A.rj by A22,A24,
PBOOLE:def 15;
B#.(p.j) = (B#*p).j by A26,FUNCT_1:13;
then reconsider g = G.j as Function of B#.pj,B.rj by A22,A25,
PBOOLE:def 15;
x.j = [[:f,g:]] by A20,A22;
hence thesis by A21,A22;
end;
hence thesis;
end;
end;
begin
::
:: Family of Many Sorted Universal Algebras
::
definition
let I,S;
mode MSAlgebra-Family of I,S -> ManySortedSet of I means
:Def5:
for i st i in I holds it.i is non-empty MSAlgebra over S;
existence
proof
set A = the non-empty MSAlgebra over S;
set f = I --> A;
reconsider f as ManySortedSet of I;
take f;
let i;
assume i in I;
hence thesis by FUNCOP_1:7;
end;
end;
definition
let I be non empty set, S;
let A be MSAlgebra-Family of I,S, i be Element of I;
redefine func A.i -> non-empty MSAlgebra over S; :: redefines . (FUNCT_1, definition)
coherence by Def5;
end;
definition
let S be non empty ManySortedSign, U1 be MSAlgebra over S;
func |.U1.| -> set equals
union (rng the Sorts of U1);
coherence;
end;
registration
let S be non empty ManySortedSign, U1 be non-empty MSAlgebra over S;
cluster |.U1.| -> non empty;
coherence
proof
reconsider St = the Sorts of U1 as non-empty ManySortedSet of the carrier
of S;
set s = the SortSymbol of S;
dom (the Sorts of U1) = the carrier of S by PARTFUN1:def 2;
then
A1: (the Sorts of U1).s in rng (the Sorts of U1) by FUNCT_1:def 3;
ex x being object st x in St.s by XBOOLE_0:def 1;
hence thesis by A1,TARSKI:def 4;
end;
end;
definition
let I be non empty set, S be non empty ManySortedSign, A be MSAlgebra-Family
of I,S;
func |.A.| -> set equals
union the set of all |.A.i.| where i is Element of I;
coherence;
end;
registration
let I be non empty set, S be non empty ManySortedSign, A be MSAlgebra-Family
of I,S;
cluster |.A.| -> non empty;
coherence
proof
set a = the Element of I;
set X = the set of all |.A.i.| where i is Element of I;
|.A.a.| in X & ex x being object st x in |.A.a.| by XBOOLE_0:def 1;
hence thesis by TARSKI:def 4;
end;
end;
begin
::
:: Product of Many Sorted Universal Algebras
::
theorem Th3:
for S be non void non empty ManySortedSign, U0 be MSAlgebra over
S, o be OperSymbol of S holds Args(o,U0) = product ((the Sorts of U0)*(
the_arity_of o)) & dom ((the Sorts of U0)*(the_arity_of o)) = dom (the_arity_of
o) & Result(o,U0) = (the Sorts of U0).(the_result_sort_of o)
proof
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, o be
OperSymbol of S;
set So = the Sorts of U0, Ar = the Arity of S, Rs = the ResultSort of S, ar
= the_arity_of o, AS = So# * Ar, RS = So * Rs, X = the carrier' of S, Cr = the
carrier of S;
A1: dom Ar = X by FUNCT_2:def 1;
then
A2: dom AS = dom Ar by PARTFUN1:def 2;
thus Args(o,U0) = AS.o by MSUALG_1:def 4
.=(So# qua ManySortedSet of Cr*).(Ar.o) by A1,A2,FUNCT_1:12
.=((So)# qua ManySortedSet of Cr*).(the_arity_of o) by MSUALG_1:def 1
.= product ((So)*(the_arity_of o)) by FINSEQ_2:def 5;
rng ar c= Cr & dom So = Cr by FINSEQ_1:def 4,PARTFUN1:def 2;
hence dom (So*ar) = dom ar by RELAT_1:27;
A3: dom Rs = X by FUNCT_2:def 1;
then
A4: dom RS = dom Rs by PARTFUN1:def 2;
thus Result(o,U0) = RS.o by MSUALG_1:def 5
.= So.(Rs.o) by A3,A4,FUNCT_1:12
.= So.the_result_sort_of o by MSUALG_1:def 2;
end;
theorem Th4:
for S be non void non empty ManySortedSign, U0 be MSAlgebra over
S, o be OperSymbol of S st the_arity_of o = {} holds Args(o,U0) = {{}}
proof
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, o be
OperSymbol of S;
assume
A1: the_arity_of o = {};
thus Args(o,U0) = product ((the Sorts of U0)*(the_arity_of o)) by Th3
.= {{}} by A1,CARD_3:10;
end;
definition
let S;
let U1,U2 be non-empty MSAlgebra over S;
func [:U1,U2:] -> MSAlgebra over S equals
MSAlgebra (# [|the Sorts of U1,the
Sorts of U2|], [[:the Charact of U1,the Charact of U2:]] #);
coherence;
end;
registration
let S;
let U1,U2 be non-empty MSAlgebra over S;
cluster [:U1,U2:] -> strict;
coherence;
end;
definition
let I,S;
let s be SortSymbol of S, A be MSAlgebra-Family of I,S;
func Carrier (A,s) -> ManySortedSet of I means
:Def9:
for i be set st i in
I ex U0 being MSAlgebra over S st U0 = A.i & it.i = (the Sorts of U0).s if I <>
{} otherwise it = {};
existence
proof
hereby
assume I <> {};
then reconsider I9 = I as non empty set;
reconsider A9 = A as MSAlgebra-Family of I9,S;
deffunc F(Element of I9) = (the Sorts of (A9.$1)).s;
consider f be Function such that
A1: dom f = I9 & for i be Element of I9 holds f.i = F(i) from
FUNCT_1:sch 4;
reconsider f as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
take f;
let i be set;
assume i in I;
then reconsider i9 = i as Element of I9;
reconsider U0 = A9.i9 as MSAlgebra over S;
take U0;
thus U0 = A.i & f.i = (the Sorts of U0).s by A1;
end;
assume
A2: I = {};
take EmptyMS I;
thus thesis by A2;
end;
uniqueness
proof
let f,g be ManySortedSet of I;
hereby
assume I <> {};
assume
A3: ( for i be set st i in I ex U0 being MSAlgebra over S st U0 = A.
i & f.i = (the Sorts of U0).s)& for i be set st i in I ex U0 being MSAlgebra
over S st U0 = A .i & g.i = (the Sorts of U0).s;
for x be object st x in I holds f.x = g.x
proof
let x be object;
assume
A4: x in I;
then reconsider i = x as Element of I;
( ex U0 being MSAlgebra over S st U0 = A.i & f.i = (the Sorts of
U0).s)& ex U0 being MSAlgebra over S st U0 = A.i & g.i = (the Sorts of U0).s
by A3,A4;
hence thesis;
end;
hence f = g;
end;
thus thesis;
end;
correctness;
end;
registration
let I,S;
let s be SortSymbol of S, A be MSAlgebra-Family of I,S;
cluster Carrier (A,s) -> non-empty;
coherence
proof
let x be object;
assume
A1: x in I;
then consider U0 being MSAlgebra over S such that
A2: U0 = A.x and
A3: Carrier (A,s).x = (the Sorts of U0).s by Def9;
U0 is non-empty MSAlgebra over S by A1,A2,Def5;
hence thesis by A3;
end;
end;
definition
let I,S;
let A be MSAlgebra-Family of I,S;
func SORTS(A) -> ManySortedSet of the carrier of S means
:Def10:
for s be SortSymbol of S holds it.s = product Carrier(A,s);
existence
proof
deffunc F(SortSymbol of S) = product Carrier(A,$1);
consider f be Function such that
A1: dom f = the carrier of S & for s be SortSymbol of S holds f.s = F(
s) from FUNCT_1:sch 4;
reconsider f as ManySortedSet of (the carrier of S) by A1,PARTFUN1:def 2
,RELAT_1:def 18;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f,g be ManySortedSet of (the carrier of S);
assume that
A2: for s be SortSymbol of S holds f.s = product Carrier(A,s) and
A3: for s be SortSymbol of S holds g.s = product Carrier(A,s);
for x be object st x in the carrier of S holds f.x = g.x
proof
let x be object;
assume x in the carrier of S;
then reconsider x1 = x as SortSymbol of S;
f.x1= product Carrier(A,x1) by A2;
hence thesis by A3;
end;
hence thesis;
end;
end;
registration
let I, S;
let A be MSAlgebra-Family of I,S;
cluster SORTS(A) -> non-empty;
coherence
proof
let x be object;
assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
(SORTS A).s = product Carrier(A,s) by Def10;
hence thesis;
end;
end;
definition
let I;
let S be non empty ManySortedSign, A be MSAlgebra-Family of I,S;
func OPER(A) -> ManySortedFunction of I means
:Def11:
for i be set st i in I
ex U0 being MSAlgebra over S st U0 = A.i & it.i = the Charact of U0 if I <> {}
otherwise it = {};
existence
proof
reconsider f = EmptyMS I as ManySortedFunction of I;
hereby
assume I <> {};
then reconsider I9 = I as non empty set;
reconsider A9 = A as MSAlgebra-Family of I9,S;
deffunc F(Element of I9) = the Charact of A9.$1;
consider X be ManySortedSet of I9 such that
A1: for i be Element of I9 holds X.i = F(i) from PBOOLE:sch 5;
for x being object st x in dom X holds X.x is Function
proof
let x be object;
assume x in dom X;
then reconsider i = x as Element of I9 by PARTFUN1:def 2;
X.i = the Charact of A9.i by A1;
hence thesis;
end;
then reconsider X as ManySortedFunction of I by FUNCOP_1:def 6;
take X;
let i be set;
assume i in I;
then reconsider i9 = i as Element of I9;
reconsider U0 = A9.i9 as MSAlgebra over S;
take U0;
thus U0 = A.i & X.i = the Charact of U0 by A1;
end;
assume
A2: I = {};
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be ManySortedFunction of I;
hereby
assume I <> {};
assume
A3: ( for i be set st i in I ex U0 being MSAlgebra over S st U0 = A.
i & f.i = the Charact of U0)& for i be set st i in I ex U0 being MSAlgebra over
S st U0 = A. i & g.i = the Charact of U0;
for x being object st x in I holds f.x = g.x
proof
let x be object;
assume
A4: x in I;
then reconsider i = x as Element of I;
( ex U0 being MSAlgebra over S st U0 = A.i & f.i = the Charact of
U0)& ex U0 being MSAlgebra over S st U0 = A.i & g.i = the Charact of U0 by A3
,A4;
hence thesis;
end;
hence f = g;
end;
thus thesis;
end;
correctness;
end;
theorem Th5:
for S be non empty ManySortedSign, A be MSAlgebra-Family of I,S
holds dom uncurry (OPER A) = [:I,the carrier' of S:]
proof
let S be non empty ManySortedSign, A be MSAlgebra-Family of I,S;
per cases;
suppose
A1: I <> {};
thus dom uncurry (OPER A) c= [:I,the carrier' of S:]
proof
let t be object;
assume t in dom uncurry (OPER A);
then consider x be object,g be Function,y be object such that
A2: t = [x,y] and
A3: x in dom (OPER A) and
A4: g = (OPER A).x & y in dom g by FUNCT_5:def 2;
reconsider x as Element of I by A3,PARTFUN1:def 2;
ex U0 being MSAlgebra over S st U0 = A.x & (OPER A).x = the Charact
of U0 by A1,Def11;
then
A5: y in the carrier' of S by A4,PARTFUN1:def 2;
x in I by A3,PARTFUN1:def 2;
hence thesis by A2,A5,ZFMISC_1:87;
end;
let x be object;
assume
A6: x in [:I,the carrier' of S:];
then consider y,z be object such that
A7: x = [y,z] by RELAT_1:def 1;
A8: z in the carrier' of S by A6,A7,ZFMISC_1:87;
reconsider y as Element of I by A6,A7,ZFMISC_1:87;
consider U0 being MSAlgebra over S such that
U0 = A.y and
A9: (OPER A).y = the Charact of U0 by A1,Def11;
dom (the Charact of U0) = the carrier' of S & dom (OPER A) = I by
PARTFUN1:def 2;
hence thesis by A1,A7,A8,A9,FUNCT_5:def 2;
end;
suppose
A10: I = {};
then OPER A = {};
hence thesis by A10,FUNCT_5:43,RELAT_1:38,ZFMISC_1:90;
end;
end;
theorem Th6:
for I be non empty set, S be non void non empty ManySortedSign,
A be MSAlgebra-Family of I,S, o be OperSymbol of S holds commute (OPER A) in
Funcs(the carrier' of S, Funcs(I,rng uncurry (OPER A)))
proof
let I be non empty set, S be non void non empty ManySortedSign, A be
MSAlgebra-Family of I,S, o be OperSymbol of S;
set f = uncurry (OPER A);
dom f = [:I,the carrier' of S:] by Th5;
then
[:I,the carrier' of S:] <> {} & f in Funcs([:I,the carrier' of S:],rng f
) by FUNCT_2:def 2,ZFMISC_1:90;
hence thesis by FUNCT_6:10;
end;
definition
let I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family
of I,S, o be OperSymbol of S;
func A?.o -> ManySortedFunction of I equals
(commute (OPER A)).o;
coherence
proof
set f = uncurry (OPER A), C = commute (OPER A);
A1: dom f = [:I,the carrier' of S:] by Th5;
per cases;
suppose
A2: I <> {};
then C in Funcs(the carrier' of S,Funcs(I,rng f)) by Th6;
then
A3: ex a be Function st a = C & dom a = the carrier' of S & rng a c=
Funcs(I,rng f) by FUNCT_2:def 2;
then C.o in rng C by FUNCT_1:def 3;
then consider g be Function such that
A4: g = C.o and
A5: dom g = I and
rng g c= rng f by A3,FUNCT_2:def 2;
reconsider g as ManySortedSet of I by A5,PARTFUN1:def 2,RELAT_1:def 18;
for x being object st x in dom g holds g.x is Function
proof
let x be object;
assume x in dom g;
then reconsider i = x as Element of I by A5;
A6: [i,o]`1 = i & [i,o]`2 = o;
consider U0 being MSAlgebra over S such that
U0 = A.i and
A7: (OPER A).i = the Charact of U0 by A2,Def11;
A8: [i,o] in dom f by A1,A2,ZFMISC_1:87;
then g.i = f.(i,o) by A4,FUNCT_5:22;
then g.i = (the Charact of U0).o by A8,A6,A7,FUNCT_5:def 2
.= Den(o,U0) by MSUALG_1:def 6;
hence thesis;
end;
hence thesis by A4,FUNCOP_1:def 6;
end;
suppose
A9: I = {};
reconsider f = EmptyMS I as ManySortedFunction of I;
f = {} by A9
.= (commute {}).o by FUNCT_6:58
.= (commute (OPER A)).o by A9;
hence thesis;
end;
end;
end;
theorem Th7:
for I be non empty set, i be Element of I, S be non void non
empty ManySortedSign, A be MSAlgebra-Family of I,S, o be OperSymbol of S holds
(A?.o).i = Den(o,A.i)
proof
let I be non empty set, i be Element of I, S be non void non empty
ManySortedSign, A be MSAlgebra-Family of I,S, o be OperSymbol of S;
set O = the carrier' of S, f = uncurry (OPER A);
A1: [i,o]`1 = i & [i,o]`2 = o;
A2: ex U0 being MSAlgebra over S st U0 = A.i & (OPER A).i = the Charact of
U0 by Def11;
A3: dom f = [:I,O:] by Th5;
then
A4: [i,o] in dom f by ZFMISC_1:87;
consider g be Function such that
A5: (curry' f).o = g and
dom g = I and
rng g c= rng f and
A6: for x st x in I holds g.x = f.(x,o) by A3,FUNCT_5:32,ZFMISC_1:90;
g.i = f.(i,o) by A6;
then g.i = (the Charact of A.i).o by A4,A1,A2,FUNCT_5:def 2
.= Den(o,A.i) by MSUALG_1:def 6;
hence thesis by A5;
end;
theorem
for I be non empty set, S be non void non empty ManySortedSign, A be
MSAlgebra-Family of I,S, o be OperSymbol of S, x be set st x in rng (Frege (A?.
o)) holds x is Function
proof
let I be non empty set, S be non void non empty ManySortedSign, A be
MSAlgebra-Family of I,S, o be OperSymbol of S, x be set;
assume x in rng (Frege (A?.o));
then ex y be object st y in dom (Frege (A?.o)) & (Frege (A?.o)).y = x by
FUNCT_1:def 3;
hence thesis;
end;
theorem Th9:
for I be non empty set, S be non void non empty ManySortedSign,
A be MSAlgebra-Family of I,S, o be OperSymbol of S, f be Function st f in rng (
Frege (A?.o)) holds dom f = I & for i be Element of I holds f.i in Result(o,A.i
)
proof
let I be non empty set, S be non void non empty ManySortedSign, A be
MSAlgebra-Family of I,S, o be OperSymbol of S, f be Function;
A1: dom (A?.o) = I by PARTFUN1:def 2;
assume f in rng (Frege (A?.o));
then consider y be object such that
A2: y in dom (Frege (A?.o)) and
A3: (Frege (A?.o)).y = f by FUNCT_1:def 3;
A4: dom (Frege (A?.o)) = product doms (A?.o) by PARTFUN1:def 2;
then consider g be Function such that
A5: g = y and
a5: dom g = dom doms (A?.o) and
A6: for i being object st i in dom doms (A?.o) holds g.i in (doms (A?.o)).i
by A2,CARD_3:def 5;
ab: dom doms (A?.o) = dom (A?.o) by FUNCT_6:def 2
.= I by PARTFUN1:def 2;
A7: f = (A?.o)..g by A2,A3,A4,A5,Def2; then
dom f = dom (A?.o) /\ dom g by PRALG_1:def 19;
hence
a8: dom f = I /\ dom g by PARTFUN1:def 2
.= I by ab,a5;
let i be Element of I;
A8: (A?.o).i = Den(o,A.i) by Th7;
dom doms(A?.o)= dom(A?.o) by FUNCT_6:def 2;
then g.i in (doms (A?.o)).i by A6,A1;
then
A9: g.i in dom Den(o,A.i) by A1,A8,FUNCT_6:22;
f.i = Den(o,A.i).(g.i) by a8,A7,A8,PRALG_1:def 19;
then
A10: f.i in rng Den(o,A.i) by A9,FUNCT_1:def 3;
rng Den(o,A.i) c= Result(o,A.i) by RELAT_1:def 19;
hence thesis by A10;
end;
theorem Th10:
for I be non empty set, S be non void non empty ManySortedSign,
A be MSAlgebra-Family of I,S, o be OperSymbol of S, f be Function st f in dom (
Frege (A?.o)) holds dom f = I & (for i be Element of I holds f.i in Args(o,A.i)
) & rng f c= Funcs(dom(the_arity_of o),|.A.|)
proof
let I be non empty set, S be non void non empty ManySortedSign, A be
MSAlgebra-Family of I,S, o be OperSymbol of S, f be Function;
assume
A1: f in dom (Frege (A?.o));
A2: dom (A?.o) = I by PARTFUN1:def 2;
A3: dom (Frege (A?.o)) = product doms (A?.o) by PARTFUN1:def 2;
A4: dom doms (A?.o) = dom(A?.o) by FUNCT_6:def 2;
hence dom f = I by A1,A3,A2,CARD_3:9;
thus
A5: for i be Element of I holds f.i in Args(o,A.i)
proof
let i be Element of I;
(A?.o).i = Den(o,A.i) & f.i in (doms(A?.o)).i by A1,A3,A2,A4,Th7,CARD_3:9;
then f.i in dom Den(o,A.i) by A2,FUNCT_6:22;
hence thesis by FUNCT_2:def 1;
end;
let x be object;
assume x in rng f;
then consider y be object such that
A6: y in dom f and
A7: x = f.y by FUNCT_1:def 3;
reconsider y as Element of I by A1,A3,A2,A4,A6,CARD_3:9;
set X = the carrier' of S, AS = (the Sorts of A.y)# * the Arity of S, Ar =
the Arity of S, Cr = the carrier of S, So = the Sorts of A.y, a = the_arity_of
o;
A8: dom Ar = X by FUNCT_2:def 1;
then
A9: dom AS = dom Ar by PARTFUN1:def 2;
A10: Args(o,A.y) = AS.o by MSUALG_1:def 4
.= (So# qua ManySortedSet of Cr*).(Ar.o) by A8,A9,FUNCT_1:12
.=(So# qua ManySortedSet of Cr*).(the_arity_of o) by MSUALG_1:def 1
.= product (So*(the_arity_of o)) by FINSEQ_2:def 5;
x in Args(o,A.y) by A5,A7;
then consider g be Function such that
A11: g = x and
A12: dom g = dom (So*a) and
A13: for i being object st i in dom (So * a) holds g.i in (So * a).i
by A10,CARD_3:def 5;
A14: rng a c= Cr & dom So = Cr by FINSEQ_1:def 4,PARTFUN1:def 2;
then
A15: dom (So * a) = dom a by RELAT_1:27;
A16: rng g c= |.A.y.|
proof
let i be object;
assume i in rng g;
then consider j being object such that
A17: j in dom g and
A18: g.j = i by FUNCT_1:def 3;
a.j in rng a by A12,A15,A17,FUNCT_1:def 3;
then
A19: So.(a.j) in rng So by A14,FUNCT_1:def 3;
i in (So * a).j by A12,A13,A17,A18;
then i in So.(a.j) by A12,A17,FUNCT_1:12;
hence thesis by A19,TARSKI:def 4;
end;
|.A.y.| in the set of all |.A.i.| where i is Element of I;
then |.A.y.| c= union the set of all |.A.i.| where i is Element of I
by ZFMISC_1:74;
then rng g c= |.A.| by A16;
hence thesis by A11,A12,A15,FUNCT_2:def 2;
end;
theorem Th11:
for I be non empty set, S be non void non empty ManySortedSign,
A be MSAlgebra-Family of I,S, o be OperSymbol of S holds dom doms (A?.o) = I &
for i be Element of I holds (doms (A?.o)).i = Args(o,A.i)
proof
let I be non empty set, S be non void non empty ManySortedSign, A be
MSAlgebra-Family of I,S, o be OperSymbol of S;
A1: dom(A?.o) = I by PARTFUN1:def 2;
for i be Element of I holds (doms (A?.o)).i = Args(o,A.i)
proof
let i be Element of I;
(A?.o).i = Den(o,A.i) by Th7;
then (doms (A?.o)).i = dom (Den(o,A.i)) by A1,FUNCT_6:22;
hence thesis by FUNCT_2:def 1;
end;
hence thesis by A1,FUNCT_6:def 2;
end;
definition
let I;
let S be non void non empty ManySortedSign, A be MSAlgebra-Family of I,S;
func OPS(A) -> ManySortedFunction of (SORTS A)# * the Arity of S, (SORTS A)
* the ResultSort of S means
for o be OperSymbol of S holds it.o=IFEQ(
the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)) if I <> {} otherwise not
contradiction;
existence
proof
defpred P[object,object] means
for o be OperSymbol of S st $1 = o holds $2 =
IFEQ(the_arity_of o,{},commute(A?.o), Commute Frege(A?.o));
set X = the carrier' of S, AS = (SORTS A)# * the Arity of S, RS = (SORTS A
) * the ResultSort of S;
A1: for x being object st x in X ex y be object st P[x,y]
proof
let x be object;
assume x in X;
then reconsider o = x as OperSymbol of S;
take IFEQ(the_arity_of o,{},commute(A?.o), Commute Frege (A?.o));
let o1 be OperSymbol of S;
assume x = o1;
hence thesis;
end;
consider f being Function such that
A2: dom f = X &
for x being object st x in X holds P[x,f.x] from CLASSES1:sch 1(A1);
reconsider f as ManySortedSet of X by A2,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 o = x as OperSymbol of S by A2;
per cases;
suppose
A3: the_arity_of o = {};
f.x = IFEQ(the_arity_of o,{},commute(A?.o), Commute Frege(A?.o)) by A2
.= commute(A?.o) by A3,FUNCOP_1:def 8;
hence thesis;
end;
suppose
A4: the_arity_of o <> {};
f.x = IFEQ(the_arity_of o,{},commute(A?.o), Commute Frege (A?.o)) by A2
.= Commute Frege (A?.o) by A4,FUNCOP_1:def 8;
hence thesis;
end;
end;
then reconsider f as ManySortedFunction of X by FUNCOP_1:def 6;
hereby
assume I <> {};
then reconsider I9 = I as non empty set;
reconsider A9 = A as MSAlgebra-Family of I9,S;
for x st x in X holds f.x is Function of AS.x,RS.x
proof
let x;
assume x in X;
then reconsider o = x as OperSymbol of S;
set ar = the_arity_of o;
set C = Commute Frege (A?.o), F = Frege (A?.o), Ar = the Arity of S,
Rs = the ResultSort of S, Cr = the carrier of S, co = commute (A?.o);
A5: rng ar c= Cr by FINSEQ_1:def 4;
A6: dom Ar = X by FUNCT_2:def 1;
then dom AS = dom Ar by PARTFUN1:def 2;
then
A7: AS.o = ((SORTS A)# qua ManySortedSet of Cr*).(Ar.o) by A6,FUNCT_1:12
.=((SORTS A)# qua ManySortedSet of Cr*).(the_arity_of o) by
MSUALG_1:def 1
.= product ((SORTS A)*(the_arity_of o)) by FINSEQ_2:def 5;
A8: dom Rs = X by FUNCT_2:def 1;
then dom RS = dom Rs by PARTFUN1:def 2;
then
A9: RS.o = (SORTS A).(Rs.o) by A8,FUNCT_1:12
.= (SORTS A).(the_result_sort_of o) by MSUALG_1:def 2
.= product Carrier(A,the_result_sort_of o) by Def10;
dom (SORTS A) = Cr by PARTFUN1:def 2;
then
A10: dom ((SORTS A)*ar) = dom ar by A5,RELAT_1:27;
per cases;
suppose
A11: the_arity_of o = {};
set rs = the_result_sort_of o;
A12: rng (A?.o) c= Funcs({{}},|.A9.|)
proof
let j be object;
assume j in rng (A?.o);
then consider a be object such that
A13: a in dom (A?.o) and
A14: (A?.o).a = j by FUNCT_1:def 3;
reconsider i = a as Element of I9 by A13,PARTFUN1:def 2;
set So = the Sorts of A9.i;
|.A9.i.| in the set of all |.A9.d.| where d is Element of I9 ;
then
A15: |.A9.i.| c= union the set of all |.A9.d.| where d is Element of I9
by ZFMISC_1:74;
dom (the Sorts of A9.i)=the carrier of S by PARTFUN1:def 2;
then So.rs in rng (the Sorts of A9.i) by FUNCT_1:def 3;
then
A16: So.rs c= union rng (the Sorts of A9.i) by ZFMISC_1:74;
rng Den(o,A9.i) c= Result(o,A9.i) & Result(o,A9.i) = So.rs by Th3,
RELAT_1:def 19;
then
A17: rng Den(o,A9.i) c= |.A9.| by A15,A16;
A18: dom Den(o,A9.i) = Args(o,A9.i) & Args(o,A9.i) = {{}} by A11,Th4,
FUNCT_2:def 1;
j = Den(o,A9.i) by A14,Th7;
hence thesis by A18,A17,FUNCT_2:def 2;
end;
dom (A?.o) = I by PARTFUN1:def 2;
then
A19: (A?.o) in Funcs(I,Funcs({{}},|.A9.|)) by A12,FUNCT_2:def 2;
then commute(A?.o) in Funcs({{}},Funcs(I,|.A9.|)) by FUNCT_6:55;
then
A20: ex h be Function st h = co & dom h = {{}} & rng h c= Funcs(I,|.
A9.|) by FUNCT_2:def 2;
A21: rng co c= RS.o
proof
let j be object;
A22: dom Carrier(A,rs) = I by PARTFUN1:def 2;
assume
A23: j in rng co;
then consider a be object such that
A24: a in dom co and
A25: co.a = j by FUNCT_1:def 3;
reconsider h = j as Function by A25;
A26: for b be object st b in dom Carrier(A,rs) holds h.b in Carrier(A
,rs).b
proof
let b be object;
assume b in dom Carrier(A,rs);
then reconsider i = b as Element of I9 by PARTFUN1:def 2;
A27: ex U0 being MSAlgebra over S st U0 = A.i & (Carrier(A,rs)).
i = (the Sorts of U0).rs by Def9;
dom Den(o,A9.i) = Args(o,A9.i) by FUNCT_2:def 1
.= {{}} by A11,Th4;
then
A28: Den(o,A9.i).a in rng Den(o,A9.i) by A20,A24,FUNCT_1:def 3;
(A?.o).i = Den (o,A9.i) by Th7;
then
A29: Den(o,A9.i).a = h.i by A19,A20,A24,A25,FUNCT_6:56;
rng Den(o,A9.i) c= Result(o,A9.i) by RELAT_1:def 19;
then h.i in Result(o,A9.i) by A29,A28;
hence thesis by A27,Th3;
end;
ex k be Function st k = h & dom k = I & rng k c= |.A9.| by A20,A23,
FUNCT_2:def 2;
hence thesis by A9,A22,A26,CARD_3:9;
end;
A30: AS.o = {{}} by A7,A11,CARD_3:10;
f.x = IFEQ(the_arity_of o,{},commute(A?.o), Commute Frege (A?.o
))by A2
.= commute(A?.o) by A11,FUNCOP_1:def 8;
hence thesis by A30,A20,A21,FUNCT_2:2;
end;
suppose
A31: the_arity_of o <> {};
A32: dom C = AS.o
proof
thus dom C c= AS.o
proof
let j be object;
assume j in dom C;
then consider g be Function such that
A33: g in dom F and
A34: j = commute g by Def1;
set cg = commute g;
A35: rng g c= Funcs(dom ar,|.A9.|) by A33,Th10;
A36: dom g = I9 by A33,Th10;
then
A37: g in Funcs(I,Funcs(dom ar,|.A9.|)) by A35,FUNCT_2:def 2;
then commute g in Funcs(dom ar,Funcs(I,|.A9.|)) by A31,FUNCT_6:55
;
then
A38: ex h be Function st h = commute g & dom h = dom ar & rng h
c= Funcs(I,|.A9.|) by FUNCT_2:def 2;
for y be object st y in dom ((SORTS A)*ar) holds cg.y in ((
SORTS A)*ar).y
proof
let y be object;
assume
A39: y in dom ((SORTS A)*ar);
then ar.y in rng ar by A10,FUNCT_1:def 3;
then reconsider s= ar.y as SortSymbol of S by A5;
cg.y in rng cg by A10,A38,A39,FUNCT_1:def 3;
then consider h be Function such that
A40: h = cg.y and
A41: dom h = I and
rng h c= |.A9.| by A38,FUNCT_2:def 2;
A42: for z be object st z in dom Carrier(A,s) holds h.z in (
Carrier(A,s)).z
proof
let z be object;
assume z in dom Carrier(A,s);
then reconsider i = z as Element of I9 by PARTFUN1:def 2;
A43: dom ((the Sorts of A9.i)# * Ar) = X by PARTFUN1:def 2;
A44: Args(o,A9.i) = ((the Sorts of A9.i)# * Ar).o by
MSUALG_1:def 4
.=((the Sorts of A9.i)# qua ManySortedSet of Cr*).(Ar.o)
by A43,FUNCT_1:12
.= ((the Sorts of A9.i)# qua ManySortedSet of Cr*).ar by
MSUALG_1:def 1
.= product((the Sorts of A9.i)*ar) by FINSEQ_2:def 5;
g.i in rng g by A36,FUNCT_1:def 3;
then consider f be Function such that
A45: f=g.i and
dom f = dom ar and
rng f c= |.A9.| by A35,FUNCT_2:def 2;
A46: ex U0 being MSAlgebra over S st U0 = A.i & (Carrier(A,s
)).i = (the Sorts of U0).s by Def9;
dom (the Sorts of A9.i) = Cr by PARTFUN1:def 2;
then
A47: dom ((the Sorts of A9.i) * ar) = dom ar by A5,RELAT_1:27;
then
A48: ((the Sorts of A9.i) * ar).y = (the Sorts of A9.i).s by A10
,A39,FUNCT_1:12;
g.i in Args(o,A9.i) by A33,Th10;
then f .y in ((the Sorts of A9.i) * ar).y by A10,A39,A45,A44
,A47,CARD_3:9;
hence thesis by A10,A37,A39,A40,A46,A45,A48,FUNCT_6:56;
end;
A49: dom Carrier(A,s) = I by PARTFUN1:def 2;
((SORTS A)*ar).y = (SORTS A).s by A39,FUNCT_1:12
.= product Carrier(A,s) by Def10;
hence thesis by A49,A40,A41,A42,CARD_3:9;
end;
hence thesis by A7,A10,A34,A38,CARD_3:9;
end;
let i be object;
assume i in AS.o;
then consider g be Function such that
A50: g = i and
A51: dom g = dom ((SORTS A)*ar) and
A52: for x being object st x in dom ((SORTS A)*ar)
holds g.x in ((SORTS A)*
ar).x by A7,CARD_3:def 5;
A53: rng g c= Funcs(I,|.A9.|)
proof
let a be object;
assume a in rng g;
then consider b be object such that
A54: b in dom g and
A55: g.b = a by FUNCT_1:def 3;
ar.b in rng ar by A10,A51,A54,FUNCT_1:def 3;
then reconsider cr = ar.b as SortSymbol of S by A5;
A56: ((SORTS A)*ar).b = (SORTS A).cr by A51,A54,FUNCT_1:12
.= product Carrier (A,cr) by Def10;
a in ((SORTS A)*ar).b by A51,A52,A54,A55;
then consider h be Function such that
A57: h = a and
A58: dom h = dom Carrier (A,cr) and
A59: for j being object st j in dom Carrier (A,cr)
holds h.j in (Carrier
(A,cr)).j by A56,CARD_3:def 5;
A60: rng h c= |.A9.|
proof
let j be object;
assume j in rng h;
then consider c be object such that
A61: c in dom h and
A62: h.c = j by FUNCT_1:def 3;
reconsider i = c as Element of I9 by A58,A61,PARTFUN1:def 2;
( ex U0 being MSAlgebra over S st U0 = A.i & (Carrier(A,
cr)).i = (the Sorts of U0).cr)& dom (the Sorts of A9.i) = the carrier of S by
Def9,PARTFUN1:def 2;
then
A63: (Carrier (A,cr)).i in rng (the Sorts of A9.i) by FUNCT_1:def 3;
h.i in (Carrier (A,cr)).i by A58,A59,A61;
then
A64: h.i in |.A9.i.| by A63,TARSKI:def 4;
|.A9.i.| in the set of all |.A9.d.| where d is Element of I9 ;
hence thesis by A62,A64,TARSKI:def 4;
end;
dom (Carrier (A,cr)) = I by PARTFUN1:def 2;
hence thesis by A57,A58,A60,FUNCT_2:def 2;
end;
then
A65: g in Funcs(dom ar,Funcs(I,|.A9.|)) by A10,A51,FUNCT_2:def 2;
then
A66: commute (commute g) = g by A31,FUNCT_6:57;
commute g in Funcs(I,Funcs(dom ar,|.A9.|)) by A31,A65,FUNCT_6:55;
then
A67: ex h be Function st h = commute g & dom h = I & rng h c=
Funcs(dom ar,|.A9.|) by FUNCT_2:def 2;
A68: for j being object st j in dom doms (A?.o)
holds (commute g).j in doms(A ?.o).j
proof
set cg = commute g;
let j be object;
assume j in dom doms (A?.o);
then reconsider ii = j as Element of I9 by Th11;
set So = the Sorts of A9.ii;
reconsider h = cg.ii as Function;
h in rng cg by A67,FUNCT_1:def 3;
then
A69: ex s be Function st s = h & dom s = dom ar & rng s c= |.A9
.| by A67,FUNCT_2:def 2;
A70: dom ((the Sorts of A9.ii)*ar) = dom ar by Th3;
A71: for a be object st a in dom (So*ar) holds h.a in (So*ar).a
proof
let a be object;
assume
A72: a in dom (So*ar);
then ar.a in rng ar by A70,FUNCT_1:def 3;
then reconsider s = ar.a as SortSymbol of S by A5;
A73: (So*ar).a = So.s by A72,FUNCT_1:12;
g.a in rng g by A10,A51,A70,A72,FUNCT_1:def 3;
then consider k be Function such that
A74: k = g.a and
dom k = I and
rng k c= |.A9.| by A53,FUNCT_2:def 2;
A75: ( ex U0 being MSAlgebra over S st U0 = A9.ii & (Carrier
(A,s)).ii = (the Sorts of U0).s)& dom (Carrier (A,s)) = I by Def9,
PARTFUN1:def 2;
A76: ((SORTS A)*ar).a = (SORTS A).s by A10,A70,A72,FUNCT_1:12
.= product Carrier (A,s) by Def10;
k.ii = h.a & k in ((SORTS A)*ar).a by A10,A52,A65,A70,A72,A74,
FUNCT_6:56;
hence thesis by A73,A76,A75,CARD_3:9;
end;
(doms (A?.o)).ii = Args(o,A9.ii) & Args(o,A9.ii) = product
((the Sorts of A9 .ii)* ar) by Th3,Th11;
hence thesis by A70,A69,A71,CARD_3:9;
end;
dom F = product doms (A?.o) & dom doms (A?.o) = I9 by Th11,
PARTFUN1:def 2;
then commute g in dom F by A67,A68,CARD_3:9;
hence thesis by A50,A66,Def1;
end;
set rs = the_result_sort_of o, CA = Carrier(A,rs);
A77: rng C c= RS.o
proof
let x be object;
A78: dom CA = I by PARTFUN1:def 2;
assume x in rng C;
then consider g be object such that
A79: g in dom C and
A80: C.g = x by FUNCT_1:def 3;
consider f be Function such that
A81: f in dom Frege(A?.o) and
A82: g = commute f by A79,Def1;
reconsider g as Function by A82;
dom f = I9 & rng f c= Funcs(dom(the_arity_of o),|.A9.|) by A81,Th10
;
then f in Funcs(I,Funcs(dom(the_arity_of o),|.A9.|)) by
FUNCT_2:def 2;
then commute g = f by A31,A82,FUNCT_6:57;
then
A83: x = F.f by A79,A80,Def1;
then reconsider h = x as Function;
A84: F.f in rng F by A81,FUNCT_1:def 3;
A85: for j being object st j in dom CA holds h.j in CA.j
proof
let j be object;
assume j in dom CA;
then reconsider i = j as Element of I9 by PARTFUN1:def 2;
A86: dom ((the Sorts of A9.i) * Rs) = dom Rs by A8,PARTFUN1:def 2;
A87: ex U0 being MSAlgebra over S st U0 = A9.i & CA.i = (the
Sorts of U0).rs by Def9;
Result(o,A9.i) = ((the Sorts of A9.i) * Rs).o by MSUALG_1:def 5
.= (the Sorts of A9.i).(Rs.o) by A8,A86,FUNCT_1:12
.= CA.i by A87,MSUALG_1:def 2;
hence thesis by A83,A84,Th9;
end;
dom h=I9 by A83,A84,Th9;
hence thesis by A9,A78,A85,CARD_3:9;
end;
f.x = IFEQ(the_arity_of o,{},commute(A?.o), Commute Frege (A?.o
))by A2
.= Commute Frege (A?.o) by A31,FUNCOP_1:def 8;
hence thesis by A32,A77,FUNCT_2:2;
end;
end;
then reconsider f as ManySortedFunction of AS,RS by PBOOLE:def 15;
take f;
let o be OperSymbol of S;
thus f.o=IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)) by A2;
end;
assume I = {};
set f = the ManySortedFunction of (SORTS A)# * the Arity of S, (SORTS A) * the
ResultSort of S;
take f;
end;
uniqueness
proof
let f,g be ManySortedFunction of (SORTS A)# * the Arity of S, (SORTS A) *
the ResultSort of S;
hereby
assume I <> {};
assume that
A88: for o be OperSymbol of S holds f.o = IFEQ(the_arity_of o,{},
commute(A?.o), Commute Frege (A?.o)) and
A89: for o be OperSymbol of S holds g.o = IFEQ(the_arity_of o,{},
commute(A?.o), Commute Frege (A?.o));
for i being object st i in the carrier' of S holds f.i = g.i
proof
let i be object;
assume i in the carrier' of S;
then reconsider o = i as Element of the carrier' of S;
f.o = IFEQ(the_arity_of o,{},commute(A?.o), Commute Frege (A?.o)
) by A88;
hence thesis by A89;
end;
hence f = g;
end;
assume
A90: I = {};
A91: now
let o be object;
assume
A92: o in the carrier' of S;
then reconsider s = (the ResultSort of S).o as SortSymbol of S by
FUNCT_2:5;
o in dom the ResultSort of S by A92,FUNCT_2:def 1;
then
A93: ((SORTS A) * the ResultSort of S).o = (SORTS A).s by FUNCT_1:13
.= product Carrier(A,s) by Def10
.= { {} } by A90,CARD_3:10;
f.o is Function of ((SORTS A)#*the Arity of S).o,((SORTS A) * the
ResultSort of S).o & g.o is Function of ((SORTS A)#*the Arity of S).o,((SORTS A
) * the ResultSort of S).o by A92,PBOOLE:def 15;
hence f.o = g.o by A93,FUNCT_2:51;
end;
thus thesis by A91;
end;
correctness;
end;
definition
let I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family
of I,S;
func product A -> MSAlgebra over S equals
MSAlgebra (# SORTS A, OPS A #);
coherence;
end;
registration
let I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family
of I,S;
cluster product A -> strict;
coherence;
end;
theorem
for S be non void non empty ManySortedSign, A be MSAlgebra-Family of I
,S holds the Sorts of product A = SORTS A & the Charact of product A = OPS A;