:: by Beata Madras

::

:: Received April 25, 1994

:: Copyright (c) 1994-2012 Association of Mizar Users

begin

registration

let X be functional non empty with_common_domain set ;

coherence

for b_{1} being Element of X holds b_{1} is DOM X -defined

end;
coherence

for b

proof end;

registration

let X be functional non empty with_common_domain set ;

coherence

for b_{1} being Element of X holds b_{1} is total

end;
coherence

for b

proof end;

begin

:: Operations on Functions

definition

let F be Function;

ex b_{1} being Function st

( ( for x being set holds

( x in dom b_{1} iff ex f being Function st

( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b_{1} holds

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

for b_{1}, b_{2} being Function st ( for x being set holds

( x in dom b_{1} iff ex f being Function st

( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b_{1} holds

b_{1} . f = F . (commute f) ) & ( for x being set holds

( x in dom b_{2} iff ex f being Function st

( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b_{2} holds

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

b_{1} = b_{2}

end;
func Commute F -> Function means :Def1: :: PRALG_2:def 1

( ( for x being set holds

( x in dom it iff ex f being Function st

( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom it holds

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

existence ( ( for x being set holds

( x in dom it iff ex f being Function st

( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom it holds

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

ex b

( ( for x being set holds

( x in dom b

( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b

b

proof end;

uniqueness for b

( x in dom b

( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b

b

( x in dom b

( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b

b

b

proof end;

:: deftheorem Def1 defines Commute PRALG_2:def 1 :

for F, b_{2} being Function holds

( b_{2} = Commute F iff ( ( for x being set holds

( x in dom b_{2} iff ex f being Function st

( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b_{2} holds

b_{2} . f = F . (commute f) ) ) );

for F, b

( b

( x in dom b

( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b

b

definition

let f be Function-yielding Function;

Frege f is ManySortedFunction of product (doms f)

for b_{1} being ManySortedFunction of product (doms f) holds

( b_{1} = Frege f iff for g being Function st g in product (doms f) holds

b_{1} . g = f .. g )

end;
:: original: Frege

redefine func Frege f -> ManySortedFunction of product (doms f) means :Def2: :: PRALG_2:def 2

for g being Function st g in product (doms f) holds

it . g = f .. g;

coherence redefine func Frege f -> ManySortedFunction of product (doms f) means :Def2: :: PRALG_2:def 2

for g being Function st g in product (doms f) holds

it . g = f .. g;

Frege f is ManySortedFunction of product (doms f)

proof end;

compatibility for b

( b

b

proof end;

:: deftheorem Def2 defines Frege PRALG_2:def 2 :

for f being Function-yielding Function

for b_{2} being ManySortedFunction of product (doms f) holds

( b_{2} = Frege f iff for g being Function st g in product (doms f) holds

b_{2} . g = f .. g );

for f being Function-yielding Function

for b

( b

b

registration
end;

theorem :: PRALG_2:2

for I being non empty set

for J being set

for A, B being ManySortedSet of I

for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]

for J being set

for A, B being ManySortedSet of I

for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]

proof end;

definition

let I be non empty set ;

let A, B be V2() ManySortedSet of I;

let pj be Element of I * ;

let rj be Element of I;

let f be Function of ((A #) . pj),(A . rj);

let g be Function of ((B #) . pj),(B . rj);

ex b_{1} being Function of (([|A,B|] #) . pj),([|A,B|] . rj) st

for h being Function st h in ([|A,B|] #) . pj holds

b_{1} . h = [(f . (pr1 h)),(g . (pr2 h))]

for b_{1}, b_{2} being Function of (([|A,B|] #) . pj),([|A,B|] . rj) st ( for h being Function st h in ([|A,B|] #) . pj holds

b_{1} . h = [(f . (pr1 h)),(g . (pr2 h))] ) & ( for h being Function st h in ([|A,B|] #) . pj holds

b_{2} . h = [(f . (pr1 h)),(g . (pr2 h))] ) holds

b_{1} = b_{2}

end;
let A, B be V2() ManySortedSet of I;

let pj be Element of I * ;

let rj be Element of I;

let f be Function of ((A #) . pj),(A . rj);

let g be Function of ((B #) . pj),(B . rj);

func [[:f,g:]] -> Function of (([|A,B|] #) . pj),([|A,B|] . rj) means :: PRALG_2:def 3

for h being Function st h in ([|A,B|] #) . pj holds

it . h = [(f . (pr1 h)),(g . (pr2 h))];

existence for h being Function st h in ([|A,B|] #) . pj holds

it . h = [(f . (pr1 h)),(g . (pr2 h))];

ex b

for h being Function st h in ([|A,B|] #) . pj holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines [[: PRALG_2:def 3 :

for I being non empty set

for A, B being V2() ManySortedSet of I

for pj being Element of I *

for rj being Element of I

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj)

for b_{8} being Function of (([|A,B|] #) . pj),([|A,B|] . rj) holds

( b_{8} = [[:f,g:]] iff for h being Function st h in ([|A,B|] #) . pj holds

b_{8} . h = [(f . (pr1 h)),(g . (pr2 h))] );

for I being non empty set

for A, B being V2() ManySortedSet of I

for pj being Element of I *

for rj being Element of I

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj)

for b

( b

b

definition

let I be non empty set ;

let J be set ;

let A, B be V2() ManySortedSet of I;

let p be Function of J,(I *);

let r be Function of J,I;

let F be ManySortedFunction of (A #) * p,A * r;

let G be ManySortedFunction of (B #) * p,B * r;

ex b_{1} being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r st

for j being set st j in J holds

for pj being Element of I *

for rj being Element of I st pj = p . j & rj = r . j holds

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds

b_{1} . j = [[:f,g:]]

for b_{1}, b_{2} being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r st ( for j being set st j in J holds

for pj being Element of I *

for rj being Element of I st pj = p . j & rj = r . j holds

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds

b_{1} . j = [[:f,g:]] ) & ( for j being set st j in J holds

for pj being Element of I *

for rj being Element of I st pj = p . j & rj = r . j holds

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds

b_{2} . j = [[:f,g:]] ) holds

b_{1} = b_{2}

end;
let J be set ;

let A, B be V2() ManySortedSet of I;

let p be Function of J,(I *);

let r be Function of J,I;

let F be ManySortedFunction of (A #) * p,A * r;

let G be ManySortedFunction of (B #) * p,B * r;

func [[:F,G:]] -> ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r means :: PRALG_2:def 4

for j being set st j in J holds

for pj being Element of I *

for rj being Element of I st pj = p . j & rj = r . j holds

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds

it . j = [[:f,g:]];

existence for j being set st j in J holds

for pj being Element of I *

for rj being Element of I st pj = p . j & rj = r . j holds

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds

it . j = [[:f,g:]];

ex b

for j being set st j in J holds

for pj being Element of I *

for rj being Element of I st pj = p . j & rj = r . j holds

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds

b

proof end;

uniqueness for b

for pj being Element of I *

for rj being Element of I st pj = p . j & rj = r . j holds

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds

b

for pj being Element of I *

for rj being Element of I st pj = p . j & rj = r . j holds

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds

b

b

proof end;

:: deftheorem defines [[: PRALG_2:def 4 :

for I being non empty set

for J being set

for A, B being V2() ManySortedSet of I

for p being Function of J,(I *)

for r being Function of J,I

for F being ManySortedFunction of (A #) * p,A * r

for G being ManySortedFunction of (B #) * p,B * r

for b_{9} being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r holds

( b_{9} = [[:F,G:]] iff for j being set st j in J holds

for pj being Element of I *

for rj being Element of I st pj = p . j & rj = r . j holds

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds

b_{9} . j = [[:f,g:]] );

for I being non empty set

for J being set

for A, B being V2() ManySortedSet of I

for p being Function of J,(I *)

for r being Function of J,I

for F being ManySortedFunction of (A #) * p,A * r

for G being ManySortedFunction of (B #) * p,B * r

for b

( b

for pj being Element of I *

for rj being Element of I st pj = p . j & rj = r . j holds

for f being Function of ((A #) . pj),(A . rj)

for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds

b

begin

::

:: Family of Many Sorted Universal Algebras

::

:: Family of Many Sorted Universal Algebras

::

definition

let I be set ;

let S be non empty ManySortedSign ;

ex b_{1} being ManySortedSet of I st

for i being set st i in I holds

b_{1} . i is non-empty MSAlgebra over S

end;
let S be non empty ManySortedSign ;

mode MSAlgebra-Family of I,S -> ManySortedSet of I means :Def5: :: PRALG_2:def 5

for i being set st i in I holds

it . i is non-empty MSAlgebra over S;

existence for i being set st i in I holds

it . i is non-empty MSAlgebra over S;

ex b

for i being set st i in I holds

b

proof end;

:: deftheorem Def5 defines MSAlgebra-Family PRALG_2:def 5 :

for I being set

for S being non empty ManySortedSign

for b_{3} being ManySortedSet of I holds

( b_{3} is MSAlgebra-Family of I,S iff for i being set st i in I holds

b_{3} . i is non-empty MSAlgebra over S );

for I being set

for S being non empty ManySortedSign

for b

( b

b

definition

let I be non empty set ;

let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

let i be Element of I;

:: original: .

redefine func A . i -> non-empty MSAlgebra over S;

coherence

A . i is non-empty MSAlgebra over S by Def5;

end;
let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

let i be Element of I;

:: original: .

redefine func A . i -> non-empty MSAlgebra over S;

coherence

A . i is non-empty MSAlgebra over S by Def5;

definition

let S be non empty ManySortedSign ;

let U1 be MSAlgebra over S;

coherence

union (rng the Sorts of U1) is set ;

end;
let U1 be MSAlgebra over S;

coherence

union (rng the Sorts of U1) is set ;

:: deftheorem defines |. PRALG_2:def 6 :

for S being non empty ManySortedSign

for U1 being MSAlgebra over S holds |.U1.| = union (rng the Sorts of U1);

for S being non empty ManySortedSign

for U1 being MSAlgebra over S holds |.U1.| = union (rng the Sorts of U1);

registration

let S be non empty ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

coherence

not |.U1.| is empty

end;
let U1 be non-empty MSAlgebra over S;

coherence

not |.U1.| is empty

proof end;

definition

let I be non empty set ;

let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

coherence

union { |.(A . i).| where i is Element of I : verum } is set ;

end;
let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

coherence

union { |.(A . i).| where i is Element of I : verum } is set ;

:: deftheorem defines |. PRALG_2:def 7 :

for I being non empty set

for S being non empty ManySortedSign

for A being MSAlgebra-Family of I,S holds |.A.| = union { |.(A . i).| where i is Element of I : verum } ;

for I being non empty set

for S being non empty ManySortedSign

for A being MSAlgebra-Family of I,S holds |.A.| = union { |.(A . i).| where i is Element of I : verum } ;

registration

let I be non empty set ;

let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

coherence

not |.A.| is empty

end;
let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

coherence

not |.A.| is empty

proof end;

begin

::

:: Product of Many Sorted Universal Algebras

::

:: Product of Many Sorted Universal Algebras

::

theorem Th3: :: PRALG_2:3

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for o being OperSymbol of S holds

( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )

for U0 being MSAlgebra over S

for o being OperSymbol of S holds

( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )

proof end;

theorem Th4: :: PRALG_2:4

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for o being OperSymbol of S st the_arity_of o = {} holds

Args (o,U0) = {{}}

for U0 being MSAlgebra over S

for o being OperSymbol of S st the_arity_of o = {} holds

Args (o,U0) = {{}}

proof end;

definition

let S be non empty ManySortedSign ;

let U1, U2 be non-empty MSAlgebra over S;

MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #) is MSAlgebra over S ;

end;
let U1, U2 be non-empty MSAlgebra over S;

func [:U1,U2:] -> MSAlgebra over S equals :: PRALG_2:def 8

MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #);

coherence MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #);

MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #) is MSAlgebra over S ;

:: deftheorem defines [: PRALG_2:def 8 :

for S being non empty ManySortedSign

for U1, U2 being non-empty MSAlgebra over S holds [:U1,U2:] = MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #);

for S being non empty ManySortedSign

for U1, U2 being non-empty MSAlgebra over S holds [:U1,U2:] = MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #);

registration

let S be non empty ManySortedSign ;

let U1, U2 be non-empty MSAlgebra over S;

coherence

[:U1,U2:] is strict ;

end;
let U1, U2 be non-empty MSAlgebra over S;

coherence

[:U1,U2:] is strict ;

definition

let I be set ;

let S be non empty ManySortedSign ;

let s be SortSymbol of S;

let A be MSAlgebra-Family of I,S;

( ( I <> {} implies ex b_{1} being ManySortedSet of I st

for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & b_{1} . i = the Sorts of U0 . s ) ) & ( not I <> {} implies ex b_{1} being ManySortedSet of I st b_{1} = {} ) )

for b_{1}, b_{2} being ManySortedSet of I holds

( ( I <> {} & ( for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & b_{1} . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & b_{2} . i = the Sorts of U0 . s ) ) implies b_{1} = b_{2} ) & ( not I <> {} & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

consistency

for b_{1} being ManySortedSet of I holds verum;

;

end;
let S be non empty ManySortedSign ;

let s be SortSymbol of S;

let A be MSAlgebra-Family of I,S;

func Carrier (A,s) -> ManySortedSet of I means :Def9: :: PRALG_2:def 9

for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & it . i = the Sorts of U0 . s ) if I <> {}

otherwise it = {} ;

existence for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & it . i = the Sorts of U0 . s ) if I <> {}

otherwise it = {} ;

( ( I <> {} implies ex b

for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & b

proof end;

uniqueness for b

( ( I <> {} & ( for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & b

ex U0 being MSAlgebra over S st

( U0 = A . i & b

proof end;

correctness consistency

for b

;

:: deftheorem Def9 defines Carrier PRALG_2:def 9 :

for I being set

for S being non empty ManySortedSign

for s being SortSymbol of S

for A being MSAlgebra-Family of I,S

for b_{5} being ManySortedSet of I holds

( ( I <> {} implies ( b_{5} = Carrier (A,s) iff for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & b_{5} . i = the Sorts of U0 . s ) ) ) & ( not I <> {} implies ( b_{5} = Carrier (A,s) iff b_{5} = {} ) ) );

for I being set

for S being non empty ManySortedSign

for s being SortSymbol of S

for A being MSAlgebra-Family of I,S

for b

( ( I <> {} implies ( b

ex U0 being MSAlgebra over S st

( U0 = A . i & b

registration

let I be set ;

let S be non empty ManySortedSign ;

let s be SortSymbol of S;

let A be MSAlgebra-Family of I,S;

coherence

Carrier (A,s) is non-empty

end;
let S be non empty ManySortedSign ;

let s be SortSymbol of S;

let A be MSAlgebra-Family of I,S;

coherence

Carrier (A,s) is non-empty

proof end;

definition

let I be set ;

let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

ex b_{1} being ManySortedSet of the carrier of S st

for s being SortSymbol of S holds b_{1} . s = product (Carrier (A,s))

for b_{1}, b_{2} being ManySortedSet of the carrier of S st ( for s being SortSymbol of S holds b_{1} . s = product (Carrier (A,s)) ) & ( for s being SortSymbol of S holds b_{2} . s = product (Carrier (A,s)) ) holds

b_{1} = b_{2}

end;
let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

func SORTS A -> ManySortedSet of the carrier of S means :Def10: :: PRALG_2:def 10

for s being SortSymbol of S holds it . s = product (Carrier (A,s));

existence for s being SortSymbol of S holds it . s = product (Carrier (A,s));

ex b

for s being SortSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines SORTS PRALG_2:def 10 :

for I being set

for S being non empty ManySortedSign

for A being MSAlgebra-Family of I,S

for b_{4} being ManySortedSet of the carrier of S holds

( b_{4} = SORTS A iff for s being SortSymbol of S holds b_{4} . s = product (Carrier (A,s)) );

for I being set

for S being non empty ManySortedSign

for A being MSAlgebra-Family of I,S

for b

( b

registration

let I be set ;

let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

coherence

SORTS A is non-empty

end;
let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

coherence

SORTS A is non-empty

proof end;

definition

let I be set ;

let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

( ( I <> {} implies ex b_{1} being ManySortedFunction of I st

for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & b_{1} . i = the Charact of U0 ) ) & ( not I <> {} implies ex b_{1} being ManySortedFunction of I st b_{1} = {} ) )

for b_{1}, b_{2} being ManySortedFunction of I holds

( ( I <> {} & ( for i being set st i in I holds

ex U0 being MSAlgebra over S st

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

ex U0 being MSAlgebra over S st

( U0 = A . i & b_{2} . i = the Charact of U0 ) ) implies b_{1} = b_{2} ) & ( not I <> {} & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

consistency

for b_{1} being ManySortedFunction of I holds verum;

;

end;
let S be non empty ManySortedSign ;

let A be MSAlgebra-Family of I,S;

func OPER A -> ManySortedFunction of I means :Def11: :: PRALG_2:def 11

for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & it . i = the Charact of U0 ) if I <> {}

otherwise it = {} ;

existence for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & it . i = the Charact of U0 ) if I <> {}

otherwise it = {} ;

( ( I <> {} implies ex b

for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & b

proof end;

uniqueness for b

( ( I <> {} & ( for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & b

ex U0 being MSAlgebra over S st

( U0 = A . i & b

proof end;

correctness consistency

for b

;

:: deftheorem Def11 defines OPER PRALG_2:def 11 :

for I being set

for S being non empty ManySortedSign

for A being MSAlgebra-Family of I,S

for b_{4} being ManySortedFunction of I holds

( ( I <> {} implies ( b_{4} = OPER A iff for i being set st i in I holds

ex U0 being MSAlgebra over S st

( U0 = A . i & b_{4} . i = the Charact of U0 ) ) ) & ( not I <> {} implies ( b_{4} = OPER A iff b_{4} = {} ) ) );

for I being set

for S being non empty ManySortedSign

for A being MSAlgebra-Family of I,S

for b

( ( I <> {} implies ( b

ex U0 being MSAlgebra over S st

( U0 = A . i & b

theorem Th5: :: PRALG_2:5

for I being set

for S being non empty ManySortedSign

for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:]

for S being non empty ManySortedSign

for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:]

proof end;

theorem Th6: :: PRALG_2:6

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A))))))

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A))))))

proof end;

definition

let I be set ;

let S be non empty non void ManySortedSign ;

let A be MSAlgebra-Family of I,S;

let o be OperSymbol of S;

coherence

(commute (OPER A)) . o is ManySortedFunction of I

end;
let S be non empty non void ManySortedSign ;

let A be MSAlgebra-Family of I,S;

let o be OperSymbol of S;

coherence

(commute (OPER A)) . o is ManySortedFunction of I

proof end;

:: deftheorem defines ?. PRALG_2:def 12 :

for I being set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S holds A ?. o = (commute (OPER A)) . o;

for I being set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S holds A ?. o = (commute (OPER A)) . o;

theorem Th7: :: PRALG_2:7

for I being non empty set

for i being Element of I

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i))

for i being Element of I

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i))

proof end;

theorem :: PRALG_2:8

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for x being set st x in rng (Frege (A ?. o)) holds

x is Function

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for x being set st x in rng (Frege (A ?. o)) holds

x is Function

proof end;

theorem Th9: :: PRALG_2:9

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for f being Function st f in rng (Frege (A ?. o)) holds

( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for f being Function st f in rng (Frege (A ?. o)) holds

( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )

proof end;

theorem Th10: :: PRALG_2:10

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for f being Function st f in dom (Frege (A ?. o)) holds

( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S

for f being Function st f in dom (Frege (A ?. o)) holds

( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )

proof end;

theorem Th11: :: PRALG_2:11

for I being non empty set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S holds

( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) )

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for o being OperSymbol of S holds

( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) )

proof end;

definition

let I be set ;

let S be non empty non void ManySortedSign ;

let A be MSAlgebra-Family of I,S;

( ( I <> {} implies ex b_{1} being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st

for o being OperSymbol of S holds b_{1} . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( not I <> {} implies ex b_{1} being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum ) )

for b_{1}, b_{2} being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds

( ( I <> {} & ( for o being OperSymbol of S holds b_{1} . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds b_{2} . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies b_{1} = b_{2} ) & ( not I <> {} implies b_{1} = b_{2} ) )

consistency

for b_{1} being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds verum;

;

end;
let S be non empty non void ManySortedSign ;

let A be MSAlgebra-Family of I,S;

func OPS A -> ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S means :: PRALG_2:def 13

for o being OperSymbol of S holds it . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) if I <> {}

otherwise verum;

existence for o being OperSymbol of S holds it . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) if I <> {}

otherwise verum;

( ( I <> {} implies ex b

for o being OperSymbol of S holds b

proof end;

uniqueness for b

( ( I <> {} & ( for o being OperSymbol of S holds b

proof end;

correctness consistency

for b

;

:: deftheorem defines OPS PRALG_2:def 13 :

for I being set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for b_{4} being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds

( ( I <> {} implies ( b_{4} = OPS A iff for o being OperSymbol of S holds b_{4} . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) ) & ( not I <> {} implies ( b_{4} = OPS A iff verum ) ) );

for I being set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S

for b

( ( I <> {} implies ( b

definition

let I be set ;

let S be non empty non void ManySortedSign ;

let A be MSAlgebra-Family of I,S;

coherence

MSAlgebra(# (SORTS A),(OPS A) #) is MSAlgebra over S ;

end;
let S be non empty non void ManySortedSign ;

let A be MSAlgebra-Family of I,S;

coherence

MSAlgebra(# (SORTS A),(OPS A) #) is MSAlgebra over S ;

:: deftheorem defines product PRALG_2:def 14 :

for I being set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S holds product A = MSAlgebra(# (SORTS A),(OPS A) #);

for I being set

for S being non empty non void ManySortedSign

for A being MSAlgebra-Family of I,S holds product A = MSAlgebra(# (SORTS A),(OPS A) #);

registration

let I be set ;

let S be non empty non void ManySortedSign ;

let A be MSAlgebra-Family of I,S;

coherence

product A is strict ;

end;
let S be non empty non void ManySortedSign ;

let A be MSAlgebra-Family of I,S;

coherence

product A is strict ;

theorem :: PRALG_2:12

:: Preliminaries

::