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

for b_{1} being FinSequence of A holds

( b_{1} = pr1 h1 iff ( len b_{1} = len h1 & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = (h1 . n) `1 ) ) )

pr1 h1 is FinSequence of A

for b_{1} being FinSequence of B holds

( b_{1} = pr2 h1 iff ( len b_{1} = len h1 & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = (h1 . n) `2 ) ) )

pr2 h1 is FinSequence of B

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

for b

( b

b

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

for b

( b

b

proof end;

coherence pr2 h1 is FinSequence of B

proof 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_{4} being FinSequence of A holds

( b_{4} = pr1 h1 iff ( len b_{4} = len h1 & ( for n being Nat st n in dom b_{4} holds

b_{4} . n = (h1 . n) `1 ) ) );

for A, B being non empty set

for h1 being FinSequence of [:A,B:]

for b

( b

b

:: deftheorem Def2 defines pr2 PRALG_1:def 2 :

for A, B being non empty set

for h1 being FinSequence of [:A,B:]

for b_{4} being FinSequence of B holds

( b_{4} = pr2 h1 iff ( len b_{4} = len h1 & ( for n being Nat st n in dom b_{4} holds

b_{4} . n = (h1 . n) `2 ) ) );

for A, B being non empty set

for h1 being FinSequence of [:A,B:]

for b

( b

b

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 ;

ex b_{1} being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st

( dom b_{1} = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b_{1} holds

b_{1} . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) )

for b_{1}, b_{2} being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st dom b_{1} = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b_{1} holds

b_{1} . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom b_{2} = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b_{2} holds

b_{2} . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) holds

b_{1} = b_{2}

end;
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 ( 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))] ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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_{5} being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] holds

( b_{5} = [[:f1,f2:]] iff ( dom b_{5} = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b_{5} holds

b_{5} . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) ) );

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

( b

b

definition

let U1, U2 be Universal_Algebra;

assume A1: U1,U2 are_similar ;

ex b_{1} being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st

( len b_{1} = len the charact of U1 & ( for n being Nat st n in dom b_{1} 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_{1} . n = [[:h1,h2:]] ) )

for b_{1}, b_{2} being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st len b_{1} = len the charact of U1 & ( for n being Nat st n in dom b_{1} 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_{1} . n = [[:h1,h2:]] ) & len b_{2} = len the charact of U1 & ( for n being Nat st n in dom b_{2} 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_{2} . n = [[:h1,h2:]] ) holds

b_{1} = b_{2}

end;
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 ( 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:]] ) );

ex b

( len b

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

proof end;

uniqueness for b

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

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

b

proof end;

:: deftheorem Def4 defines Opers PRALG_1:def 4 :

for U1, U2 being Universal_Algebra st U1,U2 are_similar holds

for b_{3} being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] holds

( b_{3} = Opers (U1,U2) iff ( len b_{3} = len the charact of U1 & ( for n being Nat st n in dom b_{3} 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_{3} . n = [[:h1,h2:]] ) ) );

for U1, U2 being Universal_Algebra st U1,U2 are_similar holds

for b

( b

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

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

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 ;

UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra by A1, Th1;

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

UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra by A1, Th1;

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

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 ;

ex b_{1} being Function of [:A,B:],[:B,A:] st

for a being Element of [:A,B:] holds b_{1} . a = [(a `2),(a `1)]

for b_{1}, b_{2} being Function of [:A,B:],[:B,A:] st ( for a being Element of [:A,B:] holds b_{1} . a = [(a `2),(a `1)] ) & ( for a being Element of [:A,B:] holds b_{2} . a = [(a `2),(a `1)] ) holds

b_{1} = b_{2}

end;
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 for a being Element of [:A,B:] holds it . a = [(a `2),(a `1)];

ex b

for a being Element of [:A,B:] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines Inv PRALG_1:def 6 :

for A, B being non empty set

for b_{3} being Function of [:A,B:],[:B,A:] holds

( b_{3} = Inv (A,B) iff for a being Element of [:A,B:] holds b_{3} . a = [(a `2),(a `1)] );

for A, B being non empty set

for b

( b

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

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

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

[:U1,U3:] is SubAlgebra of [:U2,U4:]

proof end;

begin

definition

let k be Nat;

ex b_{1} being PartFunc of ({{}} *),{{}} st

( dom b_{1} = {(k |-> {})} & rng b_{1} = {{}} )

for b_{1}, b_{2} being PartFunc of ({{}} *),{{}} st dom b_{1} = {(k |-> {})} & rng b_{1} = {{}} & dom b_{2} = {(k |-> {})} & rng b_{2} = {{}} holds

b_{1} = b_{2}
by FUNCT_1:7;

end;
func TrivialOp k -> PartFunc of ({{}} *),{{}} means :Def7: :: PRALG_1:def 7

( dom it = {(k |-> {})} & rng it = {{}} );

existence ( dom it = {(k |-> {})} & rng it = {{}} );

ex b

( dom b

proof end;

uniqueness for b

b

:: deftheorem Def7 defines TrivialOp PRALG_1:def 7 :

for k being Nat

for b_{2} being PartFunc of ({{}} *),{{}} holds

( b_{2} = TrivialOp k iff ( dom b_{2} = {(k |-> {})} & rng b_{2} = {{}} ) );

for k being Nat

for b

( b

registration

let k be Nat;

coherence

( TrivialOp k is homogeneous & TrivialOp k is quasi_total & not TrivialOp k is empty )

end;
coherence

( TrivialOp k is homogeneous & TrivialOp k is quasi_total & not TrivialOp k is empty )

proof end;

definition

let f be FinSequence of NAT ;

ex b_{1} being PFuncFinSequence of {{}} st

( len b_{1} = len f & ( for n being Nat st n in dom b_{1} holds

for m being Nat st m = f . n holds

b_{1} . n = TrivialOp m ) )

for b_{1}, b_{2} being PFuncFinSequence of {{}} st len b_{1} = len f & ( for n being Nat st n in dom b_{1} holds

for m being Nat st m = f . n holds

b_{1} . n = TrivialOp m ) & len b_{2} = len f & ( for n being Nat st n in dom b_{2} holds

for m being Nat st m = f . n holds

b_{2} . n = TrivialOp m ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( len b

for m being Nat st m = f . n holds

b

proof end;

uniqueness for b

for m being Nat st m = f . n holds

b

for m being Nat st m = f . n holds

b

b

proof end;

:: deftheorem Def8 defines TrivialOps PRALG_1:def 8 :

for f being FinSequence of NAT

for b_{2} being PFuncFinSequence of {{}} holds

( b_{2} = TrivialOps f iff ( len b_{2} = len f & ( for n being Nat st n in dom b_{2} holds

for m being Nat st m = f . n holds

b_{2} . n = TrivialOp m ) ) );

for f being FinSequence of NAT

for b

( b

for m being Nat st m = f . n holds

b

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 )

( 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

UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra

proof end;

registration

let D be non empty set ;

not for b_{1} being Element of D * holds b_{1} is empty

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

existence not for b

proof end;

definition

let f be non empty FinSequence of NAT ;

UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra by Th10;

end;
func Trivial_Algebra f -> strict Universal_Algebra equals :: PRALG_1:def 9

UAStr(# {{}},(TrivialOps f) #);

coherence UAStr(# {{}},(TrivialOps f) #);

UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra by Th10;

:: deftheorem defines Trivial_Algebra PRALG_1:def 9 :

for f being non empty FinSequence of NAT holds Trivial_Algebra f = UAStr(# {{}},(TrivialOps f) #);

for f being non empty FinSequence of NAT holds Trivial_Algebra f = UAStr(# {{}},(TrivialOps f) #);

begin

::

:: Product of Universal Algebras

::

:: Product of Universal Algebras

::

definition

let IT be Function;

end;
attr IT 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;

for x being set st x in dom IT holds

IT . x is Universal_Algebra;

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

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;

end;
attr IT 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 ;

for x being set st x in dom IT holds

IT . x is 1-sorted ;

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

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

coherence

for b_{1} being Function st b_{1} is Univ_Alg-yielding holds

b_{1} is 1-sorted-yielding

end;
for b

b

proof end;

registration
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 & y in dom IT holds

for U1, U2 being Universal_Algebra st U1 = IT . x & U2 = IT . y holds

signature U1 = signature U2 );

for IT being Function holds

( IT is equal-signature iff for x, y being set 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 ;

ex b_{1} being ManySortedSet of J st

( b_{1} is equal-signature & b_{1} is Univ_Alg-yielding )

end;
cluster Relation-like J -defined Function-like non empty total Univ_Alg-yielding equal-signature for set ;

existence ex b

( b

proof 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

end;
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;

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

end;
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;

definition

let J be set ;

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

ex b_{1} being ManySortedSet of J st

for j being set st j in J holds

ex R being 1-sorted st

( R = A . j & b_{1} . j = the carrier of R )

for b_{1}, b_{2} being ManySortedSet of J st ( for j being set st j in J holds

ex R being 1-sorted st

( R = A . j & b_{1} . j = the carrier of R ) ) & ( for j being set st j in J holds

ex R being 1-sorted st

( R = A . j & b_{2} . j = the carrier of R ) ) holds

b_{1} = b_{2}

end;
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 & it . j = the carrier of R );

existence for j being set st j in J holds

ex R being 1-sorted st

( R = A . j & it . j = the carrier of R );

ex b

for j being set st j in J holds

ex R being 1-sorted st

( R = A . j & b

proof end;

uniqueness for b

ex R being 1-sorted st

( R = A . j & b

ex R being 1-sorted st

( R = A . j & b

b

proof end;

:: deftheorem Def13 defines Carrier PRALG_1:def 13 :

for J being set

for A being 1-sorted-yielding ManySortedSet of J

for b_{3} being ManySortedSet of J holds

( b_{3} = Carrier A iff for j being set st j in J holds

ex R being 1-sorted st

( R = A . j & b_{3} . j = the carrier of R ) );

for J being set

for A being 1-sorted-yielding ManySortedSet of J

for b

( b

ex R being 1-sorted st

( R = A . j & b

registration

let J be non empty set ;

let A be Univ_Alg-yielding ManySortedSet of J;

coherence

Carrier A is non-empty

end;
let A be Univ_Alg-yielding ManySortedSet of J;

coherence

Carrier A is non-empty

proof end;

definition

let J be non empty set ;

let A be Univ_Alg-yielding equal-signature ManySortedSet of J;

ex b_{1} being FinSequence of NAT st

for j being Element of J holds b_{1} = signature (A . j)

for b_{1}, b_{2} being FinSequence of NAT st ( for j being Element of J holds b_{1} = signature (A . j) ) & ( for j being Element of J holds b_{2} = signature (A . j) ) holds

b_{1} = b_{2}

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

ex b

for j being Element of J holds b

proof end;

uniqueness for b

b

proof 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 b_{3} being FinSequence of NAT holds

( b_{3} = ComSign A iff for j being Element of J holds b_{3} = signature (A . j) );

for J being non empty set

for A being Univ_Alg-yielding equal-signature ManySortedSet of J

for b

( b

registration
end;

definition

let J be non empty set ;

let B be V2() ManySortedSet of J;

ex b_{1} being ManySortedFunction of J st

for j being Element of J holds b_{1} . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j)

end;
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 for j being Element of J holds it . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j);

ex b

for j being Element of J holds b

proof end;

:: deftheorem Def15 defines ManySortedOperation PRALG_1:def 15 :

for J being non empty set

for B being V2() ManySortedSet of J

for b_{3} being ManySortedFunction of J holds

( b_{3} is ManySortedOperation of B iff for j being Element of J holds b_{3} . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) );

for J being non empty set

for B being V2() ManySortedSet of J

for b

( b

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

definition

let IT be Function;

end;
attr IT is equal-arity means :Def16: :: PRALG_1:def 16

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;

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;

:: 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 & 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 );

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;

ex b_{1} being ManySortedOperation of B st b_{1} is equal-arity

end;
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 b

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

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;

ex b_{1} being Function st

( dom b_{1} = dom F & ( for x being set st x in dom F holds

b_{1} . x = (F . x) . (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom F & ( for x being set st x in dom F holds

b_{1} . x = (F . x) . (f . x) ) & dom b_{2} = dom F & ( for x being set st x in dom F holds

b_{2} . x = (F . x) . (f . x) ) holds

b_{1} = b_{2}

end;
let f be Function;

func F .. f -> Function means :Def17: :: PRALG_1:def 17

( dom it = dom F & ( for x being set st x in dom F holds

it . x = (F . x) . (f . x) ) );

existence ( dom it = dom F & ( for x being set st x in dom F holds

it . x = (F . x) . (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def17 defines .. PRALG_1:def 17 :

for F being Function-yielding Function

for f, b_{3} being Function holds

( b_{3} = F .. f iff ( dom b_{3} = dom F & ( for x being set st x in dom F holds

b_{3} . x = (F . x) . (f . x) ) ) );

for F being Function-yielding Function

for f, b

( b

b

registration

let I be set ;

let f be ManySortedFunction of I;

let x be ManySortedSet of I;

coherence

f .. x is I -defined

end;
let f be ManySortedFunction of I;

let x be ManySortedSet of I;

coherence

f .. x is I -defined

proof end;

registration

let I be set ;

let f be ManySortedFunction of I;

let x be ManySortedSet of I;

coherence

for b_{1} being I -defined Function st b_{1} = f .. x holds

b_{1} is total

end;
let f be ManySortedFunction of I;

let x be ManySortedSet of I;

coherence

for b

b

proof end;

definition

let I be set ;

let f be ManySortedFunction of I;

let x be ManySortedSet of I;

for b_{1} being Function holds

( b_{1} = f .. x iff ( dom b_{1} = I & ( for i being set st i in I holds

for g being Function st g = f . i holds

b_{1} . i = g . (x . i) ) ) )

end;
let f be ManySortedFunction of I;

let x be ManySortedSet of I;

:: original: ..

redefine func f .. x -> Function means :Def18: :: PRALG_1:def 18

( 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 redefine func f .. x -> Function means :Def18: :: PRALG_1:def 18

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

for b

( b

for g being Function st g = f . i holds

b

proof 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 b_{4} being Function holds

( b_{4} = f .. x iff ( dom b_{4} = I & ( for i being set st i in I holds

for g being Function st g = f . i holds

b_{4} . i = g . (x . i) ) ) );

for I being set

for f being ManySortedFunction of I

for x being ManySortedSet of I

for b

( b

for g being Function st g = f . i holds

b

registration

let J be non empty set ;

let B be V2() ManySortedSet of J;

let p be FinSequence of product B;

coherence

uncurry p is [:(dom p),J:] -defined

end;
let B be V2() ManySortedSet of J;

let p be FinSequence of product B;

coherence

uncurry p is [:(dom p),J:] -defined

proof end;

registration

let J be non empty set ;

let B be V2() ManySortedSet of J;

let p be FinSequence of product B;

coherence

for b_{1} being [:(dom p),J:] -defined Function st b_{1} = uncurry p holds

b_{1} is total

end;
let B be V2() ManySortedSet of J;

let p be FinSequence of product B;

coherence

for b

b

proof end;

registration
end;

registration

let I, J be set ;

let X be ManySortedSet of [:I,J:];

coherence

for b_{1} being [:J,I:] -defined Function st b_{1} = ~ X holds

b_{1} is total

end;
let X be ManySortedSet of [:I,J:];

coherence

for b

b

proof end;

registration

let X be set ;

let Y be non empty set ;

let f be ManySortedSet of [:X,Y:];

coherence

curry f is X -defined

end;
let Y be non empty set ;

let f be ManySortedSet of [:X,Y:];

coherence

curry f is X -defined

proof end;

registration

let X be set ;

let Y be non empty set ;

let f be ManySortedSet of [:X,Y:];

coherence

for b_{1} being X -defined Function st b_{1} = curry f holds

b_{1} is total

end;
let Y be non empty set ;

let f be ManySortedSet of [:X,Y:];

coherence

for b

b

proof end;

definition

let J be non empty set ;

let B be V2() ManySortedSet of J;

let O be equal-arity ManySortedOperation of B;

ex b_{1} being Nat st

for j being Element of J holds b_{1} = arity (O . j)

for b_{1}, b_{2} being Nat st ( for j being Element of J holds b_{1} = arity (O . j) ) & ( for j being Element of J holds b_{2} = arity (O . j) ) holds

b_{1} = b_{2}

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

ex b

for j being Element of J holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being Nat holds

( b_{4} = ComAr O iff for j being Element of J holds b_{4} = arity (O . j) );

for J being non empty set

for B being V2() ManySortedSet of J

for O being equal-arity ManySortedOperation of B

for b

( b

definition

let I be set ;

let A be ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being set st i in I holds

b_{1} . i = {} (A . i)

for b_{1}, b_{2} being ManySortedSet of I st ( for i being set st i in I holds

b_{1} . i = {} (A . i) ) & ( for i being set st i in I holds

b_{2} . i = {} (A . i) ) holds

b_{1} = b_{2}

end;
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 for i being set st i in I holds

it . i = {} (A . i);

ex b

for i being set st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def20 defines EmptySeq PRALG_1:def 20 :

for I being set

for A, b_{3} being ManySortedSet of I holds

( b_{3} = EmptySeq A iff for i being set st i in I holds

b_{3} . i = {} (A . i) );

for I being set

for A, b

( b

b

definition

let J be non empty set ;

let B be V2() ManySortedSet of J;

let O be equal-arity ManySortedOperation of B;

ex b_{1} being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) st

( dom b_{1} = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b_{1} holds

( ( dom p = {} implies b_{1} . p = O .. (EmptySeq B) ) & ( 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_{1} . p = O .. (curry w) ) ) ) )

for b_{1}, b_{2} being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) st dom b_{1} = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b_{1} holds

( ( dom p = {} implies b_{1} . p = O .. (EmptySeq B) ) & ( 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_{1} . p = O .. (curry w) ) ) ) & dom b_{2} = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b_{2} holds

( ( dom p = {} implies b_{2} . p = O .. (EmptySeq B) ) & ( 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_{2} . p = O .. (curry w) ) ) ) holds

b_{1} = b_{2}

end;
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) & ( for p being Element of (product B) * st p in dom it holds

( ( dom p = {} implies it . p = O .. (EmptySeq B) ) & ( 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 ( 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 .. (EmptySeq B) ) & ( 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) ) ) ) );

ex b

( dom b

( ( dom p = {} implies b

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

b

proof end;

uniqueness for b

( ( dom p = {} implies b

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

b

( ( dom p = {} implies b

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

b

b

proof 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 b_{4} being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) holds

( b_{4} = [[:O:]] iff ( dom b_{4} = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b_{4} holds

( ( dom p = {} implies b_{4} . p = O .. (EmptySeq B) ) & ( 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_{4} . p = O .. (curry w) ) ) ) ) );

for J being non empty set

for B being V2() ManySortedSet of J

for O being equal-arity ManySortedOperation of B

for b

( b

( ( dom p = {} implies b

for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds

b

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

ex b_{1} 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_{1} . j = o

for b_{1}, b_{2} 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_{1} . 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_{2} . j = o ) holds

b_{1} = b_{2}

end;
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 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;

ex b

for j being Element of J

for o being operation of (A . j) st the charact of (A . j) . n = o holds

b

proof end;

uniqueness for b

for o being operation of (A . j) st the charact of (A . j) . n = o holds

b

for o being operation of (A . j) st the charact of (A . j) . n = o holds

b

b

proof 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 b_{4} being equal-arity ManySortedOperation of Carrier A holds

( b_{4} = 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_{4} . j = o );

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

( b

for o being operation of (A . j) st the charact of (A . j) . n = o holds

b

definition

let J be non empty set ;

let A be Univ_Alg-yielding equal-signature ManySortedSet of J;

ex b_{1} being PFuncFinSequence of (product (Carrier A)) st

( len b_{1} = len (ComSign A) & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = [[:(ProdOp (A,n)):]] ) )

for b_{1}, b_{2} being PFuncFinSequence of (product (Carrier A)) st len b_{1} = len (ComSign A) & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = [[:(ProdOp (A,n)):]] ) & len b_{2} = len (ComSign A) & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = [[:(ProdOp (A,n)):]] ) holds

b_{1} = b_{2}

end;
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) & ( for n being Nat st n in dom it holds

it . n = [[:(ProdOp (A,n)):]] ) );

existence ( len it = len (ComSign A) & ( for n being Nat st n in dom it holds

it . n = [[:(ProdOp (A,n)):]] ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PFuncFinSequence of (product (Carrier A)) holds

( b_{3} = ProdOpSeq A iff ( len b_{3} = len (ComSign A) & ( for n being Nat st n in dom b_{3} holds

b_{3} . n = [[:(ProdOp (A,n)):]] ) ) );

for J being non empty set

for A being Univ_Alg-yielding equal-signature ManySortedSet of J

for b

( b

b

definition

let J be non empty set ;

let A be Univ_Alg-yielding equal-signature ManySortedSet of J;

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

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

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

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

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

:: Trivial Algebra

::