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

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 b₁ being FinSequence of A holds
( b₁ = pr1 h1 iff ( len b₁ = len h1 & ( for n being Nat st n in dom b₁ holds
b₁ . n = (h1 . n) `1 ) ) )

proof end;

coherence
pr1 h1 is FinSequence of A

proof end;

:: 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 b₁ being FinSequence of B holds
( b₁ = pr2 h1 iff ( len b₁ = len h1 & ( for n being Nat st n in dom b₁ holds
b₁ . n = (h1 . n) `2 ) ) )

proof end;

coherence
pr2 h1 is FinSequence of B

proof end;

end;

:: deftheorem Def1 defines pr1 PRALG_1:def 1 :
for A, B being non empty set
for h1 being FinSequence of [:A,B:]
for b₄ being FinSequence of A holds
( b₄ = pr1 h1 iff ( len b₄ = len h1 & ( for n being Nat st n in dom b₄ holds
b₄ . 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 b₄ being FinSequence of B holds
( b₄ = pr2 h1 iff ( len b₄ = len h1 & ( for n being Nat st n in dom b₄ holds
b₄ . 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 b₁ being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st
( dom b₁ = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b₁ holds
b₁ . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) )

proof end;

uniqueness
for b₁, b₂ being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st dom b₁ = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b₁ holds
b₁ . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom b₂ = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b₂ holds
b₂ . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) holds
b₁ = b₂

proof end;

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 b₅ being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] holds
( b₅ = [[:f1,f2:]] iff ( dom b₅ = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b₅ holds
b₅ . 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 b₁ being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st
( len b₁ = len the charact of U1 & ( for n being Nat st n in dom b₁ 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
b₁ . n = [[:h1,h2:]] ) )

proof end;

uniqueness
for b₁, b₂ being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st len b₁ = len the charact of U1 & ( for n being Nat st n in dom b₁ 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
b₁ . n = [[:h1,h2:]] ) & len b₂ = len the charact of U1 & ( for n being Nat st n in dom b₂ 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
b₂ . n = [[:h1,h2:]] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Opers PRALG_1:def 4 :
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
for b₃ being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] holds
( b₃ = Opers (U1,U2) iff ( len b₃ = len the charact of U1 & ( for n being Nat st n in dom b₃ 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
b₃ . 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

proof end;

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 b₁ being Function of [:A,B:],[:B,A:] st
for a being Element of [:A,B:] holds b₁ . a = [(a `2),(a `1)]

proof end;

uniqueness
for b₁, b₂ being Function of [:A,B:],[:B,A:] st ( for a being Element of [:A,B:] holds b₁ . a = [(a `2),(a `1)] ) & ( for a being Element of [:A,B:] holds b₂ . a = [(a `2),(a `1)] ) holds
b₁ = b₂

proof end;

end;

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

theorem :: PRALG_1:2

for A, B being non empty set holds rng (Inv (A,B)) = [:B,A:]

proof end;

theorem :: PRALG_1:3

for A, B being non empty set holds Inv (A,B) is one-to-one

proof end;

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:]

proof end;

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:]] )

proof end;

theorem :: PRALG_1:6

for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
[:U1,U2:],U1 are_similar

proof end;

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:]

proof end;

::
:: 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 b₁ being PartFunc of ({{}} *),{{}} st
( dom b₁ = {(k |-> {})} & rng b₁ = {{}} )

proof end;

uniqueness
for b₁, b₂ being PartFunc of ({{}} *),{{}} st dom b₁ = {(k |-> {})} & rng b₁ = {{}} & dom b₂ = {(k |-> {})} & rng b₂ = {{}} holds
b₁ = b₂ by FUNCT_1:7;

end;

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

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 )

proof end;

end;

theorem :: PRALG_1:8

for k being Nat holds arity (TrivialOp k) = k

proof end;

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 b₁ being PFuncFinSequence of {{}} st
( len b₁ = len f & ( for n being Nat st n in dom b₁ holds
for m being Nat st m = f . n holds
b₁ . n = TrivialOp m ) )

proof end;

uniqueness
for b₁, b₂ being PFuncFinSequence of {{}} st len b₁ = len f & ( for n being Nat st n in dom b₁ holds
for m being Nat st m = f . n holds
b₁ . n = TrivialOp m ) & len b₂ = len f & ( for n being Nat st n in dom b₂ holds
for m being Nat st m = f . n holds
b₂ . n = TrivialOp m ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines TrivialOps PRALG_1:def 8 :
for f being FinSequence of NAT
for b₂ being PFuncFinSequence of {{}} holds
( b₂ = TrivialOps f iff ( len b₂ = len f & ( for n being Nat st n in dom b₂ holds
for m being Nat st m = f . n holds
b₂ . 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 )

proof end;

theorem Th10: :: PRALG_1:10

for f being FinSequence of NAT st f <> {} holds
UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra

proof end;

registration

let D be non empty set ;

cluster Relation-like NAT -defined D -valued Function-like non empty V34() countable FinSequence-like FinSubsequence-like for Element of D * ;

existence
not for b₁ being Element of D * holds b₁ is empty

proof end;

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) #);

::
:: Product of Universal Algebras
::

definition

let IT be Function;

attr IT is Univ_Alg-yielding means :Def10: :: PRALG_1:def 10
for x being object 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 object st x in dom IT holds
IT . x is Universal_Algebra );

definition

let IT be Relation;

attr IT is 1-sorted-yielding means :: PRALG_1:def 11
for x being object st x in rng IT holds
x is 1-sorted ;

end;

:: deftheorem defines 1-sorted-yielding PRALG_1:def 11 :
for IT being Relation holds
( IT is 1-sorted-yielding iff for x being object st x in rng IT holds
x is 1-sorted );

definition

let IT be Function;

redefine attr IT is 1-sorted-yielding means :Def11a: :: PRALG_1:def 12
for x being object st x in dom IT holds
IT . x is 1-sorted ;

compatibility
( IT is 1-sorted-yielding iff for x being object st x in dom IT holds
IT . x is 1-sorted )

proof end;

end;

:: deftheorem Def11a defines 1-sorted-yielding PRALG_1:def 12 :
for IT being Function holds
( IT is 1-sorted-yielding iff for x being object st x in dom IT holds
IT . x is 1-sorted );

registration

cluster Relation-like Function-like Univ_Alg-yielding for set ;

existence
ex b₁ being Function st b₁ is Univ_Alg-yielding

proof end;

end;

registration

cluster Relation-like Function-like Univ_Alg-yielding -> 1-sorted-yielding for set ;

coherence
for b₁ being Function st b₁ is Univ_Alg-yielding holds
b₁ is 1-sorted-yielding ;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total 1-sorted-yielding for set ;

existence
ex b₁ being ManySortedSet of I st b₁ is 1-sorted-yielding

proof end;

end;

definition

let IT be Function;

attr IT is equal-signature means :Def12: :: PRALG_1:def 13
for x, y being object st x in dom IT & y in dom IT holds
for U1, U2 being Universal_Algebra st U1 = IT . x & U2 = IT . y holds
signature U1 = signature U2;

end;

:: deftheorem Def12 defines equal-signature PRALG_1:def 13 :
for IT being Function holds
( IT is equal-signature iff for x, y being object st x in dom IT & y in dom IT holds
for U1, U2 being Universal_Algebra st U1 = IT . x & 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 b₁ being ManySortedSet of J st
( b₁ is equal-signature & b₁ is Univ_Alg-yielding )

proof end;

end;

definition

let A be non empty 1-sorted-yielding Function;
let j be Element of dom A;
:: original: .
redefine func A . j -> 1-sorted ;
coherence
A . j is 1-sorted by Def11a;

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 func A . j -> 1-sorted ;
coherence
A . j is 1-sorted

proof end;

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 func A . j -> Universal_Algebra;
coherence
A . j is Universal_Algebra

proof end;

end;

definition

let A be 1-sorted-yielding Function;

func Carrier A -> Function means :Def13: :: PRALG_1:def 14
( dom it = dom A & ( for j being set st j in dom A holds
ex R being 1-sorted st
( R = A . j & it . j = the carrier of R ) ) );

existence
ex b₁ being Function st
( dom b₁ = dom A & ( for j being set st j in dom A holds
ex R being 1-sorted st
( R = A . j & b₁ . j = the carrier of R ) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom A & ( for j being set st j in dom A holds
ex R being 1-sorted st
( R = A . j & b₁ . j = the carrier of R ) ) & dom b₂ = dom A & ( for j being set st j in dom A holds
ex R being 1-sorted st
( R = A . j & b₂ . j = the carrier of R ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines Carrier PRALG_1:def 14 :
for A being 1-sorted-yielding Function
for b₂ being Function holds
( b₂ = Carrier A iff ( dom b₂ = dom A & ( for j being set st j in dom A holds
ex R being 1-sorted st
( R = A . j & b₂ . j = the carrier of R ) ) ) );

definition

let J be set ;
let A be 1-sorted-yielding ManySortedSet of J;

:: original: Carrier
redefine func Carrier A -> ManySortedSet of J means :: PRALG_1:def 15
for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & it . j = the carrier of R );

compatibility
for b₁ being ManySortedSet of J holds
( b₁ = Carrier A iff for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & b₁ . j = the carrier of R ) )

proof end;

coherence
Carrier A is ManySortedSet of J

proof end;

end;

:: deftheorem defines Carrier PRALG_1:def 15 :
for J being set
for A being 1-sorted-yielding ManySortedSet of J
for b₃ being ManySortedSet of J holds
( b₃ = Carrier A iff for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & b₃ . j = the carrier of R ) );

registration

let J be non empty set ;
let A be Univ_Alg-yielding ManySortedSet of J;

cluster Carrier A -> non-empty ;

coherence
Carrier A is non-empty

proof end;

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 16
for j being Element of J holds it = signature (A . j);

existence
ex b₁ being FinSequence of NAT st
for j being Element of J holds b₁ = signature (A . j)

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st ( for j being Element of J holds b₁ = signature (A . j) ) & ( for j being Element of J holds b₂ = signature (A . j) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines ComSign PRALG_1:def 16 :
for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for b₃ being FinSequence of NAT holds
( b₃ = ComSign A iff for j being Element of J holds b₃ = 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 17
for j being Element of J holds it . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j);

existence
ex b₁ being ManySortedFunction of J st
for j being Element of J holds b₁ . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)

proof end;

end;

:: deftheorem Def15 defines ManySortedOperation PRALG_1:def 17 :
for J being non empty set
for B being V2() ManySortedSet of J
for b₃ being ManySortedFunction of J holds
( b₃ is ManySortedOperation of B iff for j being Element of J holds b₃ . 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 func O . 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;

attr IT is equal-arity means :: PRALG_1:def 18
for x, y being set st x in dom IT & y in dom IT holds
for f, g being Function st IT . x = f & IT . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & 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 & g = o2 holds
arity o1 = arity o2;

end;

:: deftheorem defines equal-arity PRALG_1:def 18 :
for IT being Function holds
( IT is equal-arity iff for x, y being set st x in dom IT & y in dom IT holds
for f, g being Function st IT . x = f & IT . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & 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 & 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 V48() equal-arity for ManySortedOperation of B;

existence
ex b₁ being ManySortedOperation of B st b₁ is equal-arity

proof end;

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) )

proof end;

definition

let F be Function-yielding Function;
let f be Function;

func F .. f -> Function means :Def17: :: PRALG_1:def 19
( dom it = (dom F) /\ (dom f) & ( for x being set st x in dom it holds
it . x = (F . x) . (f . x) ) );

existence
ex b₁ being Function st
( dom b₁ = (dom F) /\ (dom f) & ( for x being set st x in dom b₁ holds
b₁ . x = (F . x) . (f . x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom F) /\ (dom f) & ( for x being set st x in dom b₁ holds
b₁ . x = (F . x) . (f . x) ) & dom b₂ = (dom F) /\ (dom f) & ( for x being set st x in dom b₂ holds
b₂ . x = (F . x) . (f . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines .. PRALG_1:def 19 :
for F being Function-yielding Function
for f, b₃ being Function holds
( b₃ = F .. f iff ( dom b₃ = (dom F) /\ (dom f) & ( for x being set st x in dom b₃ holds
b₃ . x = (F . x) . (f . x) ) ) );

registration

let I be set ;
let f be ManySortedFunction of I;
let x be ManySortedSet of I;

cluster f .. x -> I -defined ;

coherence
f .. x is I -defined

proof end;

end;

registration

let I be set ;
let f be ManySortedFunction of I;
let x be ManySortedSet of I;

cluster f .. x -> I -defined total for I -defined Function;

coherence
for b₁ being I -defined Function st b₁ = f .. x holds
b₁ is total

proof end;

end;

definition

let I be set ;
let f be ManySortedFunction of I;
let x be ManySortedSet of I;

:: original: ..
redefine func f .. x -> Function means :Def18: :: PRALG_1:def 20
( dom it = I & ( 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 b₁ being Function holds
( b₁ = f .. x iff ( dom b₁ = I & ( for i being set st i in I holds
for g being Function st g = f . i holds
b₁ . i = g . (x . i) ) ) )

proof end;

end;

:: deftheorem Def18 defines .. PRALG_1:def 20 :
for I being set
for f being ManySortedFunction of I
for x being ManySortedSet of I
for b₄ being Function holds
( b₄ = f .. x iff ( dom b₄ = I & ( for i being set st i in I holds
for g being Function st g = f . i holds
b₄ . 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

proof end;

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 b₁ being [:(dom p),J:] -defined Function st b₁ = uncurry p holds
b₁ is total

proof end;

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

proof end;

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 b₁ being [:J,I:] -defined Function st b₁ = ~ X holds
b₁ is total

proof end;

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

proof end;

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 b₁ being X -defined Function st b₁ = curry f holds
b₁ is total

proof end;

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 21
for j being Element of J holds it = arity (O . j);

existence
ex b₁ being Nat st
for j being Element of J holds b₁ = arity (O . j)

proof end;

uniqueness
for b₁, b₂ being Nat st ( for j being Element of J holds b₁ = arity (O . j) ) & ( for j being Element of J holds b₂ = arity (O . j) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines ComAr 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 b₄ being Nat holds
( b₄ = ComAr O iff for j being Element of J holds b₄ = arity (O . j) );

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 22
( 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 being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
it . p = O .. (curry w) ) ) ) );

existence
ex b₁ being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) st
( dom b₁ = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b₁ holds
( ( dom p = {} implies b₁ . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
b₁ . p = O .. (curry w) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) st dom b₁ = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b₁ holds
( ( dom p = {} implies b₁ . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
b₁ . p = O .. (curry w) ) ) ) & dom b₂ = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b₂ holds
( ( dom p = {} implies b₂ . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
b₂ . p = O .. (curry w) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines [[: PRALG_1:def 22 :
for J being non empty set
for B being V2() ManySortedSet of J
for O being equal-arity ManySortedOperation of B
for b₄ being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) holds
( b₄ = [[:O:]] iff ( dom b₄ = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b₄ holds
( ( dom p = {} implies b₄ . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
b₄ . 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 23
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 b₁ 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
b₁ . j = o

proof end;

uniqueness
for b₁, b₂ 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
b₁ . j = o ) & ( for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
b₂ . j = o ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines ProdOp PRALG_1:def 23 :
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 b₄ being equal-arity ManySortedOperation of Carrier A holds
( b₄ = 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
b₄ . 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 :Def22: :: PRALG_1:def 24
( len it = len (ComSign A) & ( for n being Nat st n in dom it holds
it . n = [[:(ProdOp (A,n)):]] ) );

existence
ex b₁ being PFuncFinSequence of (product (Carrier A)) st
( len b₁ = len (ComSign A) & ( for n being Nat st n in dom b₁ holds
b₁ . n = [[:(ProdOp (A,n)):]] ) )

proof end;

uniqueness
for b₁, b₂ being PFuncFinSequence of (product (Carrier A)) st len b₁ = len (ComSign A) & ( for n being Nat st n in dom b₁ holds
b₁ . n = [[:(ProdOp (A,n)):]] ) & len b₂ = len (ComSign A) & ( for n being Nat st n in dom b₂ holds
b₂ . n = [[:(ProdOp (A,n)):]] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines ProdOpSeq PRALG_1:def 24 :
for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for b₃ being PFuncFinSequence of (product (Carrier A)) holds
( b₃ = ProdOpSeq A iff ( len b₃ = len (ComSign A) & ( for n being Nat st n in dom b₃ holds
b₃ . 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 25
UAStr(# (product (Carrier A)),(ProdOpSeq A) #);

coherence
UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is strict Universal_Algebra

proof end;

end;

:: deftheorem defines ProdUnivAlg PRALG_1:def 25 :
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) #);