:: PRALG_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let IT be set ;
attr IT is with_common_domain means :Def1: :: PRALG_2:def 1
for f, g being Function st f in IT & g in IT holds
dom f = dom g;
end;

:: deftheorem Def1 defines with_common_domain PRALG_2:def 1 :
for IT being set holds
( IT is with_common_domain iff for f, g being Function st f in IT & g in IT holds
dom f = dom g );

registration
cluster non empty functional with_common_domain set ;
existence
ex b1 being set st
( b1 is with_common_domain & b1 is functional & not b1 is empty )
proof end;
end;

theorem :: PRALG_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{{} } is functional with_common_domain set
proof end;

definition
let X be functional with_common_domain set ;
func DOM X -> set means :Def2: :: PRALG_2:def 2
for x being Function st x in X holds
it = dom x if X <> {}
otherwise it = {} ;
existence
( ( X <> {} implies ex b1 being set st
for x being Function st x in X holds
b1 = dom x ) & ( not X <> {} implies ex b1 being set st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being set holds
( ( X <> {} & ( for x being Function st x in X holds
b1 = dom x ) & ( for x being Function st x in X holds
b2 = dom x ) implies b1 = b2 ) & ( not X <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
consistency
for b1 being set holds verum
;
end;

:: deftheorem Def2 defines DOM PRALG_2:def 2 :
for X being functional with_common_domain set
for b2 being set holds
( ( X <> {} implies ( b2 = DOM X iff for x being Function st x in X holds
b2 = dom x ) ) & ( not X <> {} implies ( b2 = DOM X iff b2 = {} ) ) );

definition
let X be non empty functional with_common_domain set ;
:: original: Element
redefine mode Element of X -> ManySortedSet of DOM X;
coherence
for b1 being Element of X holds b1 is ManySortedSet of DOM X
proof end;
end;

theorem :: PRALG_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being functional with_common_domain set st X = {{} } holds
DOM X = {}
proof end;

registration
let I be set ;
let M be V3 ManySortedSet of I;
cluster product M -> non empty functional with_common_domain ;
coherence
( product M is with_common_domain & product M is functional & not product M is empty )
proof end;
end;

definition
let F be Function;
canceled;
canceled;
canceled;
func Commute F -> Function means :Def6: :: PRALG_2:def 6
( ( 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
ex b1 being Function st
( ( for x being set holds
( x in dom b1 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b1 holds
b1 . f = F . (commute f) ) )
proof end;
uniqueness
for b1, b2 being Function st ( for x being set holds
( x in dom b1 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b1 holds
b1 . f = F . (commute f) ) & ( for x being set holds
( x in dom b2 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b2 holds
b2 . f = F . (commute f) ) holds
b1 = b2
proof end;
end;

:: deftheorem PRALG_2:def 3 :
canceled;

:: deftheorem PRALG_2:def 4 :
canceled;

:: deftheorem PRALG_2:def 5 :
canceled;

:: deftheorem Def6 defines Commute PRALG_2:def 6 :
for F, b2 being Function holds
( b2 = Commute F iff ( ( for x being set holds
( x in dom b2 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b2 holds
b2 . f = F . (commute f) ) ) );

theorem :: PRALG_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRALG_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRALG_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRALG_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRALG_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRALG_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Function st dom F = {{} } holds
Commute F = F
proof end;

definition
let f be Function-yielding Function;
canceled;
:: original: Frege
redefine func Frege f -> ManySortedFunction of product (doms f) means :Def8: :: PRALG_2:def 8
for g being Function st g in product (doms f) holds
it . g = f .. g;
coherence
Frege f is ManySortedFunction of product (doms f)
proof end;
compatibility
for b1 being ManySortedFunction of product (doms f) holds
( b1 = Frege f iff for g being Function st g in product (doms f) holds
b1 . g = f .. g )
proof end;
end;

:: deftheorem PRALG_2:def 7 :
canceled;

:: deftheorem Def8 defines Frege PRALG_2:def 8 :
for f being Function-yielding Function
for b2 being ManySortedFunction of product (doms f) holds
( b2 = Frege f iff for g being Function st g in product (doms f) holds
b2 . g = f .. g );

registration
let I be set ;
let A, B be V3 ManySortedSet of I;
cluster [|A,B|] -> V3 ;
coherence
[|A,B|] is non-empty
proof end;
end;

theorem Th9: :: PRALG_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)|]
proof end;

definition
let I be non empty set ;
let J be set ;
let A, B be V3 ManySortedSet of I;
let p be Function of J,I * ;
let r be Function of J,I;
let j be set ;
let f be Function of ((A # ) * p) . j,(A * r) . j;
let g be Function of ((B # ) * p) . j,(B * r) . j;
assume A1: j in J ;
canceled;
func [[:f,g:]] -> Function of (([|A,B|] # ) * p) . j,([|A,B|] * r) . j means :: PRALG_2:def 10
for h being Function st h in (([|A,B|] # ) * p) . j holds
it . h = [(f . (pr1 h)),(g . (pr2 h))];
existence
ex b1 being Function of (([|A,B|] # ) * p) . j,([|A,B|] * r) . j st
for h being Function st h in (([|A,B|] # ) * p) . j holds
b1 . h = [(f . (pr1 h)),(g . (pr2 h))]
proof end;
uniqueness
for b1, b2 being Function of (([|A,B|] # ) * p) . j,([|A,B|] * r) . j st ( for h being Function st h in (([|A,B|] # ) * p) . j holds
b1 . h = [(f . (pr1 h)),(g . (pr2 h))] ) & ( for h being Function st h in (([|A,B|] # ) * p) . j holds
b2 . h = [(f . (pr1 h)),(g . (pr2 h))] ) holds
b1 = b2
proof end;
end;

:: deftheorem PRALG_2:def 9 :
canceled;

:: deftheorem defines [[: PRALG_2:def 10 :
for I being non empty set
for J being set
for A, B being V3 ManySortedSet of I
for p being Function of J,I *
for r being Function of J,I
for j being set
for f being Function of ((A # ) * p) . j,(A * r) . j
for g being Function of ((B # ) * p) . j,(B * r) . j st j in J holds
for b10 being Function of (([|A,B|] # ) * p) . j,([|A,B|] * r) . j holds
( b10 = [[:f,g:]] iff for h being Function st h in (([|A,B|] # ) * p) . j holds
b10 . h = [(f . (pr1 h)),(g . (pr2 h))] );

definition
let I be non empty set ;
let J be set ;
let A, B be V3 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 11
for j being set st j in J holds
for f being Function of ((A # ) * p) . j,(A * r) . j
for g being Function of ((B # ) * p) . j,(B * r) . j st f = F . j & g = G . j holds
it . j = [[:f,g:]];
existence
ex b1 being ManySortedFunction of ([|A,B|] # ) * p,[|A,B|] * r st
for j being set st j in J holds
for f being Function of ((A # ) * p) . j,(A * r) . j
for g being Function of ((B # ) * p) . j,(B * r) . j st f = F . j & g = G . j holds
b1 . j = [[:f,g:]]
proof end;
uniqueness
for b1, b2 being ManySortedFunction of ([|A,B|] # ) * p,[|A,B|] * r st ( for j being set st j in J holds
for f being Function of ((A # ) * p) . j,(A * r) . j
for g being Function of ((B # ) * p) . j,(B * r) . j st f = F . j & g = G . j holds
b1 . j = [[:f,g:]] ) & ( for j being set st j in J holds
for f being Function of ((A # ) * p) . j,(A * r) . j
for g being Function of ((B # ) * p) . j,(B * r) . j st f = F . j & g = G . j holds
b2 . j = [[:f,g:]] ) holds
b1 = b2
proof end;
end;

:: deftheorem defines [[: PRALG_2:def 11 :
for I being non empty set
for J being set
for A, B being V3 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 b9 being ManySortedFunction of ([|A,B|] # ) * p,[|A,B|] * r holds
( b9 = [[:F,G:]] iff for j being set st j in J holds
for f being Function of ((A # ) * p) . j,(A * r) . j
for g being Function of ((B # ) * p) . j,(B * r) . j st f = F . j & g = G . j holds
b9 . j = [[:f,g:]] );

definition
let I be set ;
let S be non empty ManySortedSign ;
mode MSAlgebra-Family of I,S -> ManySortedSet of I means :Def12: :: PRALG_2:def 12
for i being set st i in I holds
it . i is non-empty MSAlgebra of S;
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is non-empty MSAlgebra of S
proof end;
end;

:: deftheorem Def12 defines MSAlgebra-Family PRALG_2:def 12 :
for I being set
for S being non empty ManySortedSign
for b3 being ManySortedSet of I holds
( b3 is MSAlgebra-Family of I,S iff for i being set st i in I holds
b3 . i is non-empty MSAlgebra of S );

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 of S;
coherence
A . i is non-empty MSAlgebra of S
by Def12;
end;

definition
let S be non empty ManySortedSign ;
let U1 be MSAlgebra of S;
func |.U1.| -> set equals :: PRALG_2:def 13
union (rng the Sorts of U1);
coherence
union (rng the Sorts of U1) is set
;
end;

:: deftheorem defines |. PRALG_2:def 13 :
for S being non empty ManySortedSign
for U1 being MSAlgebra of S holds |.U1.| = union (rng the Sorts of U1);

registration
let S be non empty ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
cluster |.U1.| -> non empty ;
coherence
not |.U1.| is empty
proof end;
end;

definition
let I be non empty set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func |.A.| -> set equals :: PRALG_2:def 14
union { |.(A . i).| where i is Element of I : verum } ;
coherence
union { |.(A . i).| where i is Element of I : verum } is set
;
end;

:: deftheorem defines |. PRALG_2:def 14 :
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;
cluster |.A.| -> non empty ;
coherence
not |.A.| is empty
proof end;
end;

theorem Th10: :: PRALG_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 Th11: :: PRALG_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 of S;
func [:U1,U2:] -> MSAlgebra of S equals :: PRALG_2:def 15
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:]] #) is MSAlgebra of S
;
end;

:: deftheorem defines [: PRALG_2:def 15 :
for S being non empty ManySortedSign
for U1, U2 being non-empty MSAlgebra of 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 of S;
cluster [:U1,U2:] -> strict ;
coherence
[:U1,U2:] is strict
;
end;

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;
func Carrier A,s -> ManySortedSet of I means :Def16: :: PRALG_2:def 16
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & it . i = the Sorts of U0 . s ) if I <> {}
otherwise it = {} ;
existence
( ( I <> {} implies ex b1 being ManySortedSet of I st
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b1 . i = the Sorts of U0 . s ) ) & ( not I <> {} implies ex b1 being ManySortedSet of I st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of I holds
( ( I <> {} & ( for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b1 . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b2 . i = the Sorts of U0 . s ) ) implies b1 = b2 ) & ( not I <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being ManySortedSet of I holds verum
;
;
end;

:: deftheorem Def16 defines Carrier PRALG_2:def 16 :
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 b5 being ManySortedSet of I holds
( ( I <> {} implies ( b5 = Carrier A,s iff for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b5 . i = the Sorts of U0 . s ) ) ) & ( not I <> {} implies ( b5 = Carrier A,s iff b5 = {} ) ) );

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;
cluster Carrier A,s -> V3 ;
coherence
Carrier A,s is non-empty
proof end;
end;

definition
let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func SORTS A -> ManySortedSet of the carrier of S means :Def17: :: PRALG_2:def 17
for s being SortSymbol of S holds it . s = product (Carrier A,s);
existence
ex b1 being ManySortedSet of the carrier of S st
for s being SortSymbol of S holds b1 . s = product (Carrier A,s)
proof end;
uniqueness
for b1, b2 being ManySortedSet of the carrier of S st ( for s being SortSymbol of S holds b1 . s = product (Carrier A,s) ) & ( for s being SortSymbol of S holds b2 . s = product (Carrier A,s) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines SORTS PRALG_2:def 17 :
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S
for b4 being ManySortedSet of the carrier of S holds
( b4 = SORTS A iff for s being SortSymbol of S holds b4 . s = product (Carrier A,s) );

registration
let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
cluster SORTS A -> V3 ;
coherence
SORTS A is non-empty
proof end;
end;

definition
let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func OPER A -> ManySortedFunction of I means :Def18: :: PRALG_2:def 18
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & it . i = the Charact of U0 ) if I <> {}
otherwise it = {} ;
existence
( ( I <> {} implies ex b1 being ManySortedFunction of I st
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b1 . i = the Charact of U0 ) ) & ( not I <> {} implies ex b1 being ManySortedFunction of I st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of I holds
( ( I <> {} & ( for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b1 . i = the Charact of U0 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b2 . i = the Charact of U0 ) ) implies b1 = b2 ) & ( not I <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being ManySortedFunction of I holds verum
;
;
end;

:: deftheorem Def18 defines OPER PRALG_2:def 18 :
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S
for b4 being ManySortedFunction of I holds
( ( I <> {} implies ( b4 = OPER A iff for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b4 . i = the Charact of U0 ) ) ) & ( not I <> {} implies ( b4 = OPER A iff b4 = {} ) ) );

theorem Th12: :: PRALG_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 OperSymbols of S:]
proof end;

theorem Th13: :: PRALG_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 OperSymbols 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;
func A ?. o -> ManySortedFunction of I equals :: PRALG_2:def 19
(commute (OPER A)) . o;
coherence
(commute (OPER A)) . o is ManySortedFunction of I
proof end;
end;

:: deftheorem defines ?. PRALG_2:def 19 :
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 Th14: :: PRALG_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: PRALG_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th16: :: PRALG_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) ) )
proof end;

theorem Th17: :: PRALG_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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.| )
proof end;

theorem Th18: :: PRALG_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) ) )
proof end;

definition
let I be set ;
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 20
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
( ( I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) # ) * the Arity of S,(SORTS A) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = IFEQ (the_arity_of o),{} ,(commute (A ?. o)),(Commute (Frege (A ?. o))) ) & ( not I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) # ) * the Arity of S,(SORTS A) * the ResultSort of S st verum ) )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of ((SORTS A) # ) * the Arity of S,(SORTS A) * the ResultSort of S holds
( ( I <> {} & ( for o being OperSymbol of S holds b1 . o = IFEQ (the_arity_of o),{} ,(commute (A ?. o)),(Commute (Frege (A ?. o))) ) & ( for o being OperSymbol of S holds b2 . o = IFEQ (the_arity_of o),{} ,(commute (A ?. o)),(Commute (Frege (A ?. o))) ) implies b1 = b2 ) & ( not I <> {} implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being ManySortedFunction of ((SORTS A) # ) * the Arity of S,(SORTS A) * the ResultSort of S holds verum
;
;
end;

:: deftheorem defines OPS PRALG_2:def 20 :
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for b4 being ManySortedFunction of ((SORTS A) # ) * the Arity of S,(SORTS A) * the ResultSort of S holds
( ( I <> {} implies ( b4 = OPS A iff for o being OperSymbol of S holds b4 . o = IFEQ (the_arity_of o),{} ,(commute (A ?. o)),(Commute (Frege (A ?. o))) ) ) & ( not I <> {} implies ( b4 = OPS A iff verum ) ) );

definition
let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func product A -> MSAlgebra of S equals :: PRALG_2:def 21
MSAlgebra(# (SORTS A),(OPS A) #);
coherence
MSAlgebra(# (SORTS A),(OPS A) #) is MSAlgebra of S
;
end;

:: deftheorem defines product PRALG_2:def 21 :
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;
cluster product A -> strict ;
coherence
product A is strict
;
end;

theorem :: PRALG_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRALG_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S holds
( the Sorts of (product A) = SORTS A & the Charact of (product A) = OPS A ) ;