:: Product of Family of Universal Algebras
:: by Beata Madras
::
:: Received October 12, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

definition
let A, B be non empty set ;
let h1 be FinSequence of [:A,B:];
:: original:pr1
redefine func pr1 h1 ->  FinSequence of A means :Def1: :: PRALG_1:def 1
( len it = len h1 & ( for n being Nat st n in dom it holds
it . n = (h1 . n) `1 ) );
compatibility
 for b1 being FinSequence of A holds
( b1 = pr1 h1 iff ( len b1 = len h1 & ( for n being Nat st n in dom b1 holds
b1 . n = (h1 . n) `1 ) ) )
proofend;
coherence
 pr1 h1 is FinSequence of A
proofend;
:: original:pr2
redefine func pr2 h1 ->  FinSequence of B means :Def2: :: PRALG_1:def 2
( len it = len h1 & ( for n being Nat st n in dom it holds
it . n = (h1 . n) `2 ) );
compatibility
 for b1 being FinSequence of B holds
( b1 = pr2 h1 iff ( len b1 = len h1 & ( for n being Nat st n in dom b1 holds
b1 . n = (h1 . n) `2 ) ) )
proofend;
coherence
 pr2 h1 is FinSequence of B
proofend;
end;

:: deftheorem Def1 defines pr1 PRALG_1:def_1_:_
 for A, B being non empty set
for h1 being FinSequence of [:A,B:]
for b4 being FinSequence of A holds
( b4 = pr1 h1 iff ( len b4 = len h1 & ( for n being Nat st n in dom b4 holds
b4 . n = (h1 . n) `1 ) ) );

:: deftheorem Def2 defines pr2 PRALG_1:def_2_:_
 for A, B being non empty set
for h1 being FinSequence of [:A,B:]
for b4 being FinSequence of B holds
( b4 = pr2 h1 iff ( len b4 = len h1 & ( for n being Nat st n in dom b4 holds
b4 . n = (h1 . n) `2 ) ) );

definition
let A, B be non empty set ;
let f1 be non empty homogeneous quasi_total PartFunc of (A *),A;
let f2 be non empty homogeneous quasi_total PartFunc of (B *),B;
assume A1: arity f1 = arity f2 ;
func[[:f1,f2:]] ->  non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] means :Def3: :: PRALG_1:def 3
( dom it = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom it holds
it . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) );
existence
 ex b1 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st
( dom b1 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b1 holds
b1 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) )
proofend;
uniqueness
 for b1, b2 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st dom b1 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b1 holds
b1 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom b2 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b2 holds
b2 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines [[: PRALG_1:def_3_:_
 for A, B being non empty set
for f1 being non empty homogeneous quasi_total PartFunc of (A *),A
for f2 being non empty homogeneous quasi_total PartFunc of (B *),B st arity f1 = arity f2 holds
for b5 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] holds
( b5 = [[:f1,f2:]] iff ( dom b5 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b5 holds
b5 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) ) );

definition
let U1, U2 be Universal_Algebra;
assume A1: U1,U2 are_similar ;
func Opers (U1,U2) ->  PFuncFinSequence of [: the carrier of U1, the carrier of U2:] means :Def4: :: PRALG_1:def 4
( len it = len the charact of U1 & ( for n being Nat st n in dom it holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
it . n = [[:h1,h2:]] ) );
existence
 ex b1 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st
( len b1 = len the charact of U1 & ( for n being Nat st n in dom b1 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b1 . n = [[:h1,h2:]] ) )
proofend;
uniqueness
 for b1, b2 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st len b1 = len the charact of U1 & ( for n being Nat st n in dom b1 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b1 . n = [[:h1,h2:]] ) & len b2 = len the charact of U1 & ( for n being Nat st n in dom b2 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b2 . n = [[:h1,h2:]] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines Opers PRALG_1:def_4_:_
 for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
for b3 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] holds
( b3 = Opers (U1,U2) iff ( len b3 = len the charact of U1 & ( for n being Nat st n in dom b3 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b3 . n = [[:h1,h2:]] ) ) );

theorem Th1: :: PRALG_1:1
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra
proofend;

definition
let U1, U2 be Universal_Algebra;
assume A1: U1,U2 are_similar ;
func[:U1,U2:] ->  strict Universal_Algebra equals :Def5: :: PRALG_1:def 5
 UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #);
coherence
 UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra by A1, Th1;
end;

:: deftheorem Def5 defines [: PRALG_1:def_5_:_
 for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
[:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #);

definition
let A, B be non empty set ;
func Inv (A,B) ->  Function of [:A,B:],[:B,A:] means :Def6: :: PRALG_1:def 6
 for a being Element of [:A,B:] holds it . a = [(a `2),(a `1)];
existence
 ex b1 being Function of [:A,B:],[:B,A:] st
for a being Element of [:A,B:] holds b1 . a = [(a `2),(a `1)]
proofend;
uniqueness
 for b1, b2 being Function of [:A,B:],[:B,A:] st ( for a being Element of [:A,B:] holds b1 . a = [(a `2),(a `1)] ) & ( for a being Element of [:A,B:] holds b2 . a = [(a `2),(a `1)] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines Inv PRALG_1:def_6_:_
 for A, B being non empty set
for b3 being Function of [:A,B:],[:B,A:] holds
( b3 = Inv (A,B) iff for a being Element of [:A,B:] holds b3 . a = [(a `2),(a `1)] );

theorem :: PRALG_1:2
for A, B being non empty set holds rng (Inv (A,B)) = [:B,A:]
proofend;

theorem :: PRALG_1:3
for A, B being non empty set holds Inv (A,B) is one-to-one
proofend;

theorem :: PRALG_1:4
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
Inv ( the carrier of U1, the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:]
proofend;

theorem Th5: :: PRALG_1:5
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
for o1 being operation of U1
for o2 being operation of U2
for o being operation of [:U1,U2:]
for n being 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:]] )
proofend;

theorem :: PRALG_1:6
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
[:U1,U2:],U1 are_similar
proofend;

theorem :: PRALG_1:7
for U1, U2, U3, U4 being 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:]
proofend;

begin

::
:: Trivial Algebra
::
definition
let k be Nat;
func TrivialOp k ->  PartFunc of ({{}} *),{{}} means :Def7: :: PRALG_1:def 7
( dom it = {(k |-> {})} & rng it = {{}} );
existence
 ex b1 being PartFunc of ({{}} *),{{}} st
( dom b1 = {(k |-> {})} & rng b1 = {{}} )
proofend;
uniqueness
 for b1, b2 being PartFunc of ({{}} *),{{}} st dom b1 = {(k |-> {})} & rng b1 = {{}} & dom b2 = {(k |-> {})} & rng b2 = {{}} holds
b1 = b2 by FUNCT_1:7;
end;

:: deftheorem Def7 defines TrivialOp PRALG_1:def_7_:_
 for k being Nat
for b2 being PartFunc of ({{}} *),{{}} holds
( b2 = TrivialOp k iff ( dom b2 = {(k |-> {})} & rng b2 = {{}} ) );

registration
let k be Nat;
cluster TrivialOp k ->  non empty homogeneous quasi_total ;
coherence
 ( TrivialOp k is homogeneous & TrivialOp k is quasi_total & not TrivialOp k is empty )
proofend;
end;

theorem :: PRALG_1:8
for k being Nat holds arity (TrivialOp k) = k
proofend;

definition
let f be FinSequence of NAT ;
func TrivialOps f ->  PFuncFinSequence of {{}} means :Def8: :: PRALG_1:def 8
( len it = len f & ( for n being Nat st n in dom it holds
for m being Nat st m = f . n holds
it . n = TrivialOp m ) );
existence
 ex b1 being PFuncFinSequence of {{}} st
( len b1 = len f & ( for n being Nat st n in dom b1 holds
for m being Nat st m = f . n holds
b1 . n = TrivialOp m ) )
proofend;
uniqueness
 for b1, b2 being PFuncFinSequence of {{}} st len b1 = len f & ( for n being Nat st n in dom b1 holds
for m being Nat st m = f . n holds
b1 . n = TrivialOp m ) & len b2 = len f & ( for n being Nat st n in dom b2 holds
for m being Nat st m = f . n holds
b2 . n = TrivialOp m ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines TrivialOps PRALG_1:def_8_:_
 for f being FinSequence of NAT
for b2 being PFuncFinSequence of {{}} holds
( b2 = TrivialOps f iff ( len b2 = len f & ( for n being Nat st n in dom b2 holds
for m being Nat st m = f . n holds
b2 . n = TrivialOp m ) ) );

theorem Th9: :: PRALG_1:9
for f being FinSequence of NAT holds
( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty )
proofend;

theorem Th10: :: PRALG_1:10
for f being FinSequence of NAT st f <> {} holds
UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra
proofend;

registration
let D be non empty set ;
cluster Relation-like NAT -defined D -valued Function-like non empty V31() countable FinSequence-like FinSubsequence-like for Element of D * ;
existence
 not for b1 being Element of D * holds b1 is empty
proofend;
end;

definition
let f be non empty FinSequence of NAT ;
func Trivial_Algebra f ->  strict Universal_Algebra equals :: PRALG_1:def 9
 UAStr(# {{}},(TrivialOps f) #);
coherence
 UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra by Th10;
end;

:: deftheorem  defines Trivial_Algebra PRALG_1:def_9_:_
 for f being non empty FinSequence of NAT holds Trivial_Algebra f = UAStr(# {{}},(TrivialOps f) #);

begin

::
:: Product of Universal Algebras
::
definition
let IT be Function;
attrIT is Univ_Alg-yielding  means :Def10: :: PRALG_1:def 10
 for x being set st x in dom IT holds
IT . x is Universal_Algebra;
end;

:: deftheorem Def10 defines Univ_Alg-yielding PRALG_1:def_10_:_
 for IT being Function holds
( IT is Univ_Alg-yielding iff for x being set st x in dom IT holds
IT . x is Universal_Algebra );

definition
let IT be Function;
attrIT is 1-sorted-yielding  means :Def11: :: PRALG_1:def 11
 for x being set st x in dom IT holds
IT . x is 1-sorted ;
end;

:: deftheorem Def11 defines 1-sorted-yielding PRALG_1:def_11_:_
 for IT being Function holds
( IT is 1-sorted-yielding iff for x being set st x in dom IT holds
IT . x is 1-sorted );

registration
cluster Relation-like Function-like Univ_Alg-yielding for set ;
existence
 ex b1 being Function st b1 is Univ_Alg-yielding
proofend;
end;

registration
cluster Relation-like Function-like Univ_Alg-yielding  ->  1-sorted-yielding for set ;
coherence
 for b1 being Function st b1 is Univ_Alg-yielding holds
b1 is 1-sorted-yielding
proofend;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total 1-sorted-yielding for set ;
existence
 ex b1 being ManySortedSet of I st b1 is 1-sorted-yielding
proofend;
end;

definition
let IT be Function;
attrIT is equal-signature  means :Def12: :: PRALG_1:def 12
 for x, y being set st x in dom IT &amp; y in dom IT holds
for U1, U2 being Universal_Algebra st U1 = IT . x &amp; U2 = IT . y holds
signature U1 = signature U2;
end;

:: deftheorem Def12 defines equal-signature PRALG_1:def_12_:_
 for IT being Function holds
( IT is equal-signature iff for x, y being set st x in dom IT &amp; y in dom IT holds
for U1, U2 being Universal_Algebra st U1 = IT . x &amp; U2 = IT . y holds
signature U1 = signature U2 );

registration
let J be non empty set ;
cluster Relation-like J -defined Function-like non empty total Univ_Alg-yielding equal-signature for set ;
existence
 ex b1 being ManySortedSet of J st
( b1 is equal-signature &amp; b1 is Univ_Alg-yielding )
proofend;
end;

definition
let J be non empty set ;
let A be 1-sorted-yielding ManySortedSet of J;
let j be Element of J;
:: original:.
redefine funcA . j ->  1-sorted ;
coherence
 A . j is 1-sorted
proofend;
end;

definition
let J be non empty set ;
let A be Univ_Alg-yielding ManySortedSet of J;
let j be Element of J;
:: original:.
redefine funcA . j ->  Universal_Algebra;
coherence
 A . j is Universal_Algebra
proofend;
end;

definition
let J be set ;
let A be 1-sorted-yielding ManySortedSet of J;
func Carrier A ->  ManySortedSet of J means :Def13: :: PRALG_1:def 13
 for j being set st j in J holds
ex R being 1-sorted st
( R = A . j &amp; it . j = the carrier of R );
existence
 ex b1 being ManySortedSet of J st
for j being set st j in J holds
ex R being 1-sorted st
( R = A . j &amp; b1 . j = the carrier of R )
proofend;
uniqueness
 for b1, b2 being ManySortedSet of J st ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j &amp; b1 . j = the carrier of R ) ) &amp; ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j &amp; b2 . j = the carrier of R ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines Carrier PRALG_1:def_13_:_
 for J being set
for A being 1-sorted-yielding ManySortedSet of J
for b3 being ManySortedSet of J holds
( b3 = Carrier A iff for j being set st j in J holds
ex R being 1-sorted st
( R = A . j &amp; b3 . j = the carrier of R ) );

registration
let J be non empty set ;
let A be Univ_Alg-yielding ManySortedSet of J;
cluster Carrier A -> V2() ;
coherence
 Carrier A is non-empty
proofend;
end;

definition
let J be non empty set ;
let A be Univ_Alg-yielding equal-signature ManySortedSet of J;
func ComSign A ->  FinSequence of NAT  means :Def14: :: PRALG_1:def 14
 for j being Element of J holds it = signature (A . j);
existence
 ex b1 being FinSequence of NAT st
for j being Element of J holds b1 = signature (A . j)
proofend;
uniqueness
 for b1, b2 being FinSequence of NAT st ( for j being Element of J holds b1 = signature (A . j) ) &amp; ( for j being Element of J holds b2 = signature (A . j) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines ComSign PRALG_1:def_14_:_
 for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for b3 being FinSequence of NAT holds
( b3 = ComSign A iff for j being Element of J holds b3 = signature (A . j) );

registration
let J be non empty set ;
let B be V2() ManySortedSet of J;
cluster product B ->  non empty ;
coherence
 not product B is empty ;
end;

definition
let J be non empty set ;
let B be V2() ManySortedSet of J;
mode ManySortedOperation of B ->  ManySortedFunction of J means :Def15: :: PRALG_1:def 15
 for j being Element of J holds it . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j);
existence
 ex b1 being ManySortedFunction of J st
for j being Element of J holds b1 . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)
proofend;
end;

:: deftheorem Def15 defines ManySortedOperation PRALG_1:def_15_:_
 for J being non empty set
for B being V2() ManySortedSet of J
for b3 being ManySortedFunction of J holds
( b3 is ManySortedOperation of B iff for j being Element of J holds b3 . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) );

definition
let J be non empty set ;
let B be V2() ManySortedSet of J;
let O be ManySortedOperation of B;
let j be Element of J;
:: original:.
redefine funcO . j ->  non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j);
coherence
 O . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) by Def15;
end;

definition
let IT be Function;
attrIT is equal-arity  means :Def16: :: PRALG_1:def 16
 for x, y being set st x in dom IT &amp; y in dom IT holds
for f, g being Function st IT . x = f &amp; IT . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X &amp; dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 &amp; g = o2 holds
arity o1 = arity o2;
end;

:: deftheorem Def16 defines equal-arity PRALG_1:def_16_:_
 for IT being Function holds
( IT is equal-arity iff for x, y being set st x in dom IT &amp; y in dom IT holds
for f, g being Function st IT . x = f &amp; IT . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X &amp; dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 &amp; g = o2 holds
arity o1 = arity o2 );

registration
let J be non empty set ;
let B be V2() ManySortedSet of J;
cluster Relation-like J -defined Function-like non empty total Function-yielding V45() equal-arity for ManySortedOperation of B;
existence
 ex b1 being ManySortedOperation of B st b1 is equal-arity
proofend;
end;

theorem Th11: :: PRALG_1:11
for J being non empty set
for B being V2() ManySortedSet of J
for O being ManySortedOperation of B holds
( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) )
proofend;

definition
let F be Function-yielding Function;
let f be Function;
funcF .. f ->  Function means :Def17: :: PRALG_1:def 17
( dom it = dom F &amp; ( for x being set st x in dom F holds
it . x = (F . x) . (f . x) ) );
existence
 ex b1 being Function st
( dom b1 = dom F &amp; ( for x being set st x in dom F holds
b1 . x = (F . x) . (f . x) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom F &amp; ( for x being set st x in dom F holds
b1 . x = (F . x) . (f . x) ) &amp; dom b2 = dom F &amp; ( for x being set st x in dom F holds
b2 . x = (F . x) . (f . x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines .. PRALG_1:def_17_:_
 for F being Function-yielding Function
for f, b3 being Function holds
( b3 = F .. f iff ( dom b3 = dom F &amp; ( for x being set st x in dom F holds
b3 . x = (F . x) . (f . x) ) ) );

registration
let I be set ;
let f be ManySortedFunction of I;
let x be ManySortedSet of I;
clusterf .. x -> I -defined ;
coherence
 f .. x is I -defined
proofend;
end;

registration
let I be set ;
let f be ManySortedFunction of I;
let x be ManySortedSet of I;
clusterf .. x -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = f .. x holds
b1 is total
proofend;
end;

definition
let I be set ;
let f be ManySortedFunction of I;
let x be ManySortedSet of I;
:: original:..
redefine funcf .. x ->  Function means :Def18: :: PRALG_1:def 18
( dom it = I &amp; ( for i being set st i in I holds
for g being Function st g = f . i holds
it . i = g . (x . i) ) );
compatibility
 for b1 being Function holds
( b1 = f .. x iff ( dom b1 = I &amp; ( for i being set st i in I holds
for g being Function st g = f . i holds
b1 . i = g . (x . i) ) ) )
proofend;
end;

:: deftheorem Def18 defines .. PRALG_1:def_18_:_
 for I being set
for f being ManySortedFunction of I
for x being ManySortedSet of I
for b4 being Function holds
( b4 = f .. x iff ( dom b4 = I &amp; ( for i being set st i in I holds
for g being Function st g = f . i holds
b4 . i = g . (x . i) ) ) );

registration
let J be non empty set ;
let B be V2() ManySortedSet of J;
let p be FinSequence of product B;
cluster uncurry p -> [:(dom p),J:] -defined ;
coherence
 uncurry p is [:(dom p),J:] -defined
proofend;
end;

registration
let J be non empty set ;
let B be V2() ManySortedSet of J;
let p be FinSequence of product B;
cluster uncurry p -> [:(dom p),J:] -defined total for [:(dom p),J:] -defined Function;
coherence
 for b1 being [:(dom p),J:] -defined Function st b1 = uncurry p holds
b1 is total
proofend;
end;

registration
let I, J be set ;
let X be ManySortedSet of [:I,J:];
cluster ~ X -> [:J,I:] -defined ;
coherence
 ~ X is [:J,I:] -defined
proofend;
end;

registration
let I, J be set ;
let X be ManySortedSet of [:I,J:];
cluster ~ X -> [:J,I:] -defined total for [:J,I:] -defined Function;
coherence
 for b1 being [:J,I:] -defined Function st b1 = ~ X holds
b1 is total
proofend;
end;

registration
let X be set ;
let Y be non empty set ;
let f be ManySortedSet of [:X,Y:];
cluster curry f -> X -defined ;
coherence
 curry f is X -defined
proofend;
end;

registration
let X be set ;
let Y be non empty set ;
let f be ManySortedSet of [:X,Y:];
cluster curry f -> X -defined total for X -defined Function;
coherence
 for b1 being X -defined Function st b1 = curry f holds
b1 is total
proofend;
end;

definition
let J be non empty set ;
let B be V2() ManySortedSet of J;
let O be equal-arity ManySortedOperation of B;
func ComAr O ->  Nat means :Def19: :: PRALG_1:def 19
 for j being Element of J holds it = arity (O . j);
existence
 ex b1 being Nat st
for j being Element of J holds b1 = arity (O . j)
proofend;
uniqueness
 for b1, b2 being Nat st ( for j being Element of J holds b1 = arity (O . j) ) &amp; ( for j being Element of J holds b2 = arity (O . j) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines ComAr PRALG_1:def_19_:_
 for J being non empty set
for B being V2() ManySortedSet of J
for O being equal-arity ManySortedOperation of B
for b4 being Nat holds
( b4 = ComAr O iff for j being Element of J holds b4 = arity (O . j) );

definition
let I be set ;
let A be ManySortedSet of I;
func EmptySeq A ->  ManySortedSet of I means :Def20: :: PRALG_1:def 20
 for i being set st i in I holds
it . i = {} (A . i);
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = {} (A . i)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = {} (A . i) ) &amp; ( for i being set st i in I holds
b2 . i = {} (A . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def20 defines EmptySeq PRALG_1:def_20_:_
 for I being set
for A, b3 being ManySortedSet of I holds
( b3 = EmptySeq A iff for i being set st i in I holds
b3 . i = {} (A . i) );

definition
let J be non empty set ;
let B be V2() ManySortedSet of J;
let O be equal-arity ManySortedOperation of B;
func[[:O:]] ->  non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) means :: PRALG_1:def 21
( dom it = (ComAr O) -tuples_on (product B) &amp; ( for p being Element of (product B) * st p in dom it holds
( ( dom p = {} implies it . p = O .. (EmptySeq B) ) &amp; ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p &amp; w = ~ (uncurry p) holds
it . p = O .. (curry w) ) ) ) );
existence
 ex b1 being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) st
( dom b1 = (ComAr O) -tuples_on (product B) &amp; ( for p being Element of (product B) * st p in dom b1 holds
( ( dom p = {} implies b1 . p = O .. (EmptySeq B) ) &amp; ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p &amp; w = ~ (uncurry p) holds
b1 . p = O .. (curry w) ) ) ) )
proofend;
uniqueness
 for b1, b2 being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) st dom b1 = (ComAr O) -tuples_on (product B) &amp; ( for p being Element of (product B) * st p in dom b1 holds
( ( dom p = {} implies b1 . p = O .. (EmptySeq B) ) &amp; ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p &amp; w = ~ (uncurry p) holds
b1 . p = O .. (curry w) ) ) ) &amp; dom b2 = (ComAr O) -tuples_on (product B) &amp; ( for p being Element of (product B) * st p in dom b2 holds
( ( dom p = {} implies b2 . p = O .. (EmptySeq B) ) &amp; ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p &amp; w = ~ (uncurry p) holds
b2 . p = O .. (curry w) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines [[: PRALG_1:def_21_:_
 for J being non empty set
for B being V2() ManySortedSet of J
for O being equal-arity ManySortedOperation of B
for b4 being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) holds
( b4 = [[:O:]] iff ( dom b4 = (ComAr O) -tuples_on (product B) &amp; ( for p being Element of (product B) * st p in dom b4 holds
( ( dom p = {} implies b4 . p = O .. (EmptySeq B) ) &amp; ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p &amp; w = ~ (uncurry p) holds
b4 . p = O .. (curry w) ) ) ) ) );

definition
let J be non empty set ;
let A be Univ_Alg-yielding equal-signature ManySortedSet of J;
let n be Nat;
assume A1: n in dom (ComSign A) ;
func ProdOp (A,n) ->  equal-arity ManySortedOperation of Carrier A means :: PRALG_1:def 22
 for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
it . j = o;
existence
 ex b1 being equal-arity ManySortedOperation of Carrier A st
for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
b1 . j = o
proofend;
uniqueness
 for b1, b2 being equal-arity ManySortedOperation of Carrier A st ( for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
b1 . j = o ) &amp; ( for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
b2 . j = o ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines ProdOp PRALG_1:def_22_:_
 for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for n being Nat st n in dom (ComSign A) holds
for b4 being equal-arity ManySortedOperation of Carrier A holds
( b4 = ProdOp (A,n) iff for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
b4 . j = o );

definition
let J be non empty set ;
let A be Univ_Alg-yielding equal-signature ManySortedSet of J;
func ProdOpSeq A ->  PFuncFinSequence of (product (Carrier A)) means :Def23: :: PRALG_1:def 23
( len it = len (ComSign A) &amp; ( for n being Nat st n in dom it holds
it . n = [[:(ProdOp (A,n)):]] ) );
existence
 ex b1 being PFuncFinSequence of (product (Carrier A)) st
( len b1 = len (ComSign A) &amp; ( for n being Nat st n in dom b1 holds
b1 . n = [[:(ProdOp (A,n)):]] ) )
proofend;
uniqueness
 for b1, b2 being PFuncFinSequence of (product (Carrier A)) st len b1 = len (ComSign A) &amp; ( for n being Nat st n in dom b1 holds
b1 . n = [[:(ProdOp (A,n)):]] ) &amp; len b2 = len (ComSign A) &amp; ( for n being Nat st n in dom b2 holds
b2 . n = [[:(ProdOp (A,n)):]] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def23 defines ProdOpSeq PRALG_1:def_23_:_
 for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for b3 being PFuncFinSequence of (product (Carrier A)) holds
( b3 = ProdOpSeq A iff ( len b3 = len (ComSign A) &amp; ( for n being Nat st n in dom b3 holds
b3 . n = [[:(ProdOp (A,n)):]] ) ) );

definition
let J be non empty set ;
let A be Univ_Alg-yielding equal-signature ManySortedSet of J;
func ProdUnivAlg A ->  strict Universal_Algebra equals :: PRALG_1:def 24
 UAStr(# (product (Carrier A)),(ProdOpSeq A) #);
coherence
 UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is strict Universal_Algebra
proofend;
end;

:: deftheorem  defines ProdUnivAlg PRALG_1:def_24_:_
 for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J holds ProdUnivAlg A = UAStr(# (product (Carrier A)),(ProdOpSeq A) #);