:: MSUALG_1 semantic presentation

begin

 begin

definition
attrc1 is strict ;
struct ManySortedSign  ->  2-sorted ;
aggrManySortedSign(# carrier, carrier', Arity, ResultSort #) ->  ManySortedSign ;
sel Arity c1 ->  Function of the carrier' of c1,( the carrier of c1 *);
sel ResultSort c1 ->  Function of the carrier' of c1, the carrier of c1;
end;

registration
cluster non empty void strict for ManySortedSign ;
existence
 ex b1 being ManySortedSign st
( b1 is void & b1 is strict & not b1 is empty )
proof
reconsider g = {} --> {} as Function of {},{{}} ;
reconsider f = {} --> {} as Function of {},({{}} *) ;
take  ManySortedSign(# {{}},{},f,g #) ; ::_thesis: ( ManySortedSign(# {{}},{},f,g #) is void & ManySortedSign(# {{}},{},f,g #) is strict & not ManySortedSign(# {{}},{},f,g #) is empty )
thus  ( ManySortedSign(# {{}},{},f,g #) is void & ManySortedSign(# {{}},{},f,g #) is strict & not ManySortedSign(# {{}},{},f,g #) is empty ) ; ::_thesis: verum
end;
cluster non empty non void strict for ManySortedSign ;
existence
 ex b1 being ManySortedSign st
( not b1 is void & b1 is strict & not b1 is empty )
proof
 {} in {{}} * by FINSEQ_1:49;
then reconsider f = {{}} --> {} as Function of {{}},({{}} *) by FUNCOP_1:46;
reconsider g = {{}} --> {} as Function of {{}},{{}} ;
take  ManySortedSign(# {{}},{{}},f,g #) ; ::_thesis: ( not ManySortedSign(# {{}},{{}},f,g #) is void & ManySortedSign(# {{}},{{}},f,g #) is strict & not ManySortedSign(# {{}},{{}},f,g #) is empty )
thus  ( not ManySortedSign(# {{}},{{}},f,g #) is void & ManySortedSign(# {{}},{{}},f,g #) is strict & not ManySortedSign(# {{}},{{}},f,g #) is empty ) ; ::_thesis: verum
end;
end;

definition
let S be non empty ManySortedSign ;
mode SortSymbol of S is Element of S;
mode OperSymbol of S is Element of the carrier' of S;
end;

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
func the_arity_of o ->  Element of the carrier of S *  equals :: MSUALG_1:def 1
 the Arity of S . o;
coherence
 the Arity of S . o is Element of the carrier of S * ;
func the_result_sort_of o ->  Element of S equals :: MSUALG_1:def 2
 the ResultSort of S . o;
coherence
 the ResultSort of S . o is Element of S ;
end;

:: deftheorem  defines the_arity_of MSUALG_1:def_1_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S holds the_arity_of o = the Arity of S . o;

:: deftheorem  defines the_result_sort_of MSUALG_1:def_2_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S holds the_result_sort_of o = the ResultSort of S . o;

begin

definition
let S be 1-sorted ;
attrc2 is strict ;
struct many-sorted over S -> ;
aggrmany-sorted(# Sorts #) ->  many-sorted over S;
sel Sorts c2 ->  ManySortedSet of the carrier of S;
end;

definition
let S be non empty ManySortedSign ;
attrc2 is strict ;
struct MSAlgebra over S ->  many-sorted over S;
aggrMSAlgebra(# Sorts, Charact #) ->  MSAlgebra over S;
sel Charact c2 ->  ManySortedFunction of ( the Sorts of c2 #) * the Arity of S, the Sorts of c2 * the ResultSort of S;
end;

definition
let S be 1-sorted ;
let A be many-sorted over S;
attrA is non-empty  means :Def3: :: MSUALG_1:def 3
 the Sorts of A is V5();
end;

:: deftheorem Def3 defines non-empty MSUALG_1:def_3_:_
 for S being 1-sorted
for A being many-sorted over S holds
( A is non-empty iff the Sorts of A is V5() );

registration
let S be non empty ManySortedSign ;
cluster strict non-empty for MSAlgebra over S;
existence
 ex b1 being MSAlgebra over S st
( b1 is strict & b1 is non-empty )
proof
reconsider s = the carrier of S --> {0} as ManySortedSet of the carrier of S ;
set o = the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S;
take  MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) ; ::_thesis: ( MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) is strict & MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) is non-empty )
thus  MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) is strict ; ::_thesis: MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) is non-empty
let i be set ; :: according to PBOOLE:def_13,MSUALG_1:def_3 ::_thesis: ( not i in the carrier of S or not the Sorts of MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) . i is empty )
assume  i in the carrier of S ; ::_thesis: not the Sorts of MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) . i is empty
hence  not the Sorts of MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) . i is empty ; ::_thesis: verum
end;
end;

registration
let S be 1-sorted ;
cluster strict non-empty for many-sorted over S;
existence
 ex b1 being many-sorted over S st
( b1 is strict & b1 is non-empty )
proof
reconsider s = the carrier of S --> {0} as ManySortedSet of the carrier of S ;
take  many-sorted(# s #) ; ::_thesis: ( many-sorted(# s #) is strict & many-sorted(# s #) is non-empty )
thus  many-sorted(# s #) is strict ; ::_thesis: many-sorted(# s #) is non-empty
let i be set ; :: according to PBOOLE:def_13,MSUALG_1:def_3 ::_thesis: ( not i in the carrier of S or not the Sorts of many-sorted(# s #) . i is empty )
assume  i in the carrier of S ; ::_thesis: not the Sorts of many-sorted(# s #) . i is empty
hence  not the Sorts of many-sorted(# s #) . i is empty ; ::_thesis: verum
end;
end;

registration
let S be 1-sorted ;
let A be non-empty many-sorted over S;
cluster the Sorts of A -> V5() ;
coherence
 the Sorts of A is non-empty by Def3;
end;

registration
let S be non empty ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster  ->  non empty for Element of rng the Sorts of A;
coherence
 for b1 being Component of the Sorts of A holds not b1 is empty
proof
let C be Component of the Sorts of A; ::_thesis: not C is empty
 ex i being set st
( i in the carrier of S & C = the Sorts of A . i ) by PBOOLE:138;
hence  not C is empty ; ::_thesis: verum
end;
cluster  ->  non empty for Element of rng ( the Sorts of A #);
coherence
 for b1 being Component of ( the Sorts of A #) holds not b1 is empty
proof
let C be Component of ( the Sorts of A #); ::_thesis: not C is empty
 ex i being set st
( i in the carrier of S * & C = ( the Sorts of A #) . i ) by PBOOLE:138;
hence  not C is empty ; ::_thesis: verum
end;
end;

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be MSAlgebra over S;
func Args (o,A) ->  Component of ( the Sorts of A #) equals :: MSUALG_1:def 4
(( the Sorts of A #) * the Arity of S) . o;
coherence
 (( the Sorts of A #) * the Arity of S) . o is Component of ( the Sorts of A #)
proof
 o in the carrier' of S ;
then  o in dom (( the Sorts of A #) * the Arity of S) by PARTFUN1:def_2;
then  (( the Sorts of A #) * the Arity of S) . o in rng (( the Sorts of A #) * the Arity of S) by FUNCT_1:def_3;
hence  (( the Sorts of A #) * the Arity of S) . o is Component of ( the Sorts of A #) by FUNCT_1:14; ::_thesis: verum
end;
correctness
;
func Result (o,A) ->  Component of the Sorts of A equals :: MSUALG_1:def 5
( the Sorts of A * the ResultSort of S) . o;
coherence
 ( the Sorts of A * the ResultSort of S) . o is Component of the Sorts of A
proof
 o in the carrier' of S ;
then  o in dom ( the Sorts of A * the ResultSort of S) by PARTFUN1:def_2;
then  ( the Sorts of A * the ResultSort of S) . o in rng ( the Sorts of A * the ResultSort of S) by FUNCT_1:def_3;
hence  ( the Sorts of A * the ResultSort of S) . o is Component of the Sorts of A by FUNCT_1:14; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines Args MSUALG_1:def_4_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra over S holds Args (o,A) = (( the Sorts of A #) * the Arity of S) . o;

:: deftheorem  defines Result MSUALG_1:def_5_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra over S holds Result (o,A) = ( the Sorts of A * the ResultSort of S) . o;

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be MSAlgebra over S;
func Den (o,A) ->  Function of (Args (o,A)),(Result (o,A)) equals :: MSUALG_1:def 6
 the Charact of A . o;
coherence
 the Charact of A . o is Function of (Args (o,A)),(Result (o,A)) by PBOOLE:def_15;
end;

:: deftheorem  defines Den MSUALG_1:def_6_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra over S holds Den (o,A) = the Charact of A . o;

theorem :: MSUALG_1:1
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S holds not Den (o,A) is empty ;

begin

  Lm1:  for D being non empty set
for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = (arity h) -tuples_on D
proof
let D be non empty set ; ::_thesis: for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = (arity h) -tuples_on D
let h be non empty homogeneous quasi_total PartFunc of (D *),D; ::_thesis: dom h = (arity h) -tuples_on D
set x0 = the Element of dom h;
A1: the Element of dom h in dom h ;
A2: dom h c= D * by RELAT_1:def_18;
then reconsider x0 = the Element of dom h as FinSequence of D by A1, FINSEQ_1:def_11;
thus  dom h c= (arity h) -tuples_on D :: according to XBOOLE_0:def_10 ::_thesis: (arity h) -tuples_on D c= dom h
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom h or x in (arity h) -tuples_on D )
assume A3: x in dom h ; ::_thesis: x in (arity h) -tuples_on D
then reconsider f = x as FinSequence of D by A2, FINSEQ_1:def_11;
A4: f is Element of (len f) -tuples_on D by FINSEQ_2:92;
 len f = arity h by A3, MARGREL1:def_25;
hence  x in (arity h) -tuples_on D by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (arity h) -tuples_on D or x in dom h )
assume  x in (arity h) -tuples_on D ; ::_thesis: x in dom h
then reconsider f = x as Element of (arity h) -tuples_on D ;
len x0 = arity h by MARGREL1:def_25
.= len f by CARD_1:def_7 ;
hence  x in dom h by MARGREL1:def_22; ::_thesis: verum
end;

theorem Th2: :: MSUALG_1:2
for C being set
for A, B being non empty set
for F being PartFunc of C,A
for G being Function of A,B holds G * F is Function of (dom F),B
proof
let C be set ; ::_thesis: for A, B being non empty set
for F being PartFunc of C,A
for G being Function of A,B holds G * F is Function of (dom F),B
let A, B be non empty set ; ::_thesis: for F being PartFunc of C,A
for G being Function of A,B holds G * F is Function of (dom F),B
let F be PartFunc of C,A; ::_thesis: for G being Function of A,B holds G * F is Function of (dom F),B
let G be Function of A,B; ::_thesis: G * F is Function of (dom F),B
 dom G = A by FUNCT_2:def_1;
then  rng F c= dom G by RELAT_1:def_19;
then A1: dom (G * F) = dom F by RELAT_1:27;
 rng (G * F) c= B by RELAT_1:def_19;
hence  G * F is Function of (dom F),B by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;

theorem Th3: :: MSUALG_1:3
for D being non empty set
for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = Funcs ((Seg (arity h)),D)
proof
let D be non empty set ; ::_thesis: for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = Funcs ((Seg (arity h)),D)
let h be non empty homogeneous quasi_total PartFunc of (D *),D; ::_thesis: dom h = Funcs ((Seg (arity h)),D)
thus  dom h = (arity h) -tuples_on D by Lm1
.= Funcs ((Seg (arity h)),D) by FINSEQ_2:93 ; ::_thesis: verum
end;

theorem Th4: :: MSUALG_1:4
for A being Universal_Algebra holds not signature A is empty
proof
let A be Universal_Algebra; ::_thesis: not signature A is empty
 len the charact of A <> 0 ;
then  len (signature A) <> 0 by UNIALG_1:def_4;
hence  not signature A is empty ; ::_thesis: verum
end;

begin

definition
let IT be ManySortedSign ;
attrIT is segmental  means :Def7: :: MSUALG_1:def 7
 ex n being Nat st the carrier' of IT = Seg n;
end;

:: deftheorem Def7 defines segmental MSUALG_1:def_7_:_
 for IT being ManySortedSign holds
( IT is segmental iff ex n being Nat st the carrier' of IT = Seg n );

theorem Th5: :: MSUALG_1:5
for S being non empty ManySortedSign st S is trivial holds
for A being MSAlgebra over S
for c1, c2 being Component of the Sorts of A holds c1 = c2
proof
let S be non empty ManySortedSign ; ::_thesis: ( S is trivial implies for A being MSAlgebra over S
for c1, c2 being Component of the Sorts of A holds c1 = c2 )
assume A1: S is trivial ; ::_thesis: for A being MSAlgebra over S
for c1, c2 being Component of the Sorts of A holds c1 = c2
let A be MSAlgebra over S; ::_thesis: for c1, c2 being Component of the Sorts of A holds c1 = c2
let c1, c2 be Component of the Sorts of A; ::_thesis: c1 = c2
 ( ex i1 being set st
( i1 in the carrier of S & c1 = the Sorts of A . i1 ) & ex i2 being set st
( i2 in the carrier of S & c2 = the Sorts of A . i2 ) ) by PBOOLE:138;
hence  c1 = c2 by A1, STRUCT_0:def_10; ::_thesis: verum
end;

reconsider z = 0 as Element of {0} by TARSKI:def_1;

Lm2:  for A being Universal_Algebra
for f being Function of (dom (signature A)),({0} *) holds
( ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is 1 -element & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict )
proof
let A be Universal_Algebra; ::_thesis: for f being Function of (dom (signature A)),({0} *) holds
( ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is 1 -element & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict )
let f be Function of (dom (signature A)),({0} *); ::_thesis: ( ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is 1 -element & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict )
set S = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #);
A1: ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental
proof
take  len (signature A) ; :: according to MSUALG_1:def_7 ::_thesis: the carrier' of ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) = Seg (len (signature A))
thus  the carrier' of ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) = Seg (len (signature A)) by FINSEQ_1:def_3; ::_thesis: verum
end;
 signature A <> {} by Th4;
hence  ( ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is 1 -element & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict ) by A1, STRUCT_0:def_19; ::_thesis: verum
end;

registration
cluster non void 1 -element strict segmental for ManySortedSign ;
existence
 ex b1 being ManySortedSign st
( b1 is segmental & not b1 is void & b1 is strict & b1 is 1 -element )
proof
set A = the Universal_Algebra;
reconsider f = (*--> 0) * (signature the Universal_Algebra) as Function of (dom (signature the Universal_Algebra)),({0} *) by Th2;
 ( ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is segmental & not ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is void & ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is strict & ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is 1 -element ) by Lm2;
hence  ex b1 being ManySortedSign st
( b1 is segmental & not b1 is void & b1 is strict & b1 is 1 -element ) ; ::_thesis: verum
end;
end;

definition
let A be Universal_Algebra;
func MSSign A ->  trivial non void strict segmental ManySortedSign  means :Def8: :: MSUALG_1:def 8
( the carrier of it = {0} & the carrier' of it = dom (signature A) & the Arity of it = (*--> 0) * (signature A) & the ResultSort of it = (dom (signature A)) --> 0 );
correctness
existence
ex b1 being trivial non void strict segmental ManySortedSign st
( the carrier of b1 = {0} & the carrier' of b1 = dom (signature A) & the Arity of b1 = (*--> 0) * (signature A) & the ResultSort of b1 = (dom (signature A)) --> 0 );
uniqueness
for b1, b2 being trivial non void strict segmental ManySortedSign st the carrier of b1 = {0} & the carrier' of b1 = dom (signature A) & the Arity of b1 = (*--> 0) * (signature A) & the ResultSort of b1 = (dom (signature A)) --> 0 & the carrier of b2 = {0} & the carrier' of b2 = dom (signature A) & the Arity of b2 = (*--> 0) * (signature A) & the ResultSort of b2 = (dom (signature A)) --> 0 holds
b1 = b2;
proof
reconsider f = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by Th2;
 ( ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is trivial & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict ) by Lm2;
hence  ( ex b1 being trivial non void strict segmental ManySortedSign st
( the carrier of b1 = {0} & the carrier' of b1 = dom (signature A) & the Arity of b1 = (*--> 0) * (signature A) & the ResultSort of b1 = (dom (signature A)) --> 0 ) & ( for b1, b2 being trivial non void strict segmental ManySortedSign st the carrier of b1 = {0} & the carrier' of b1 = dom (signature A) & the Arity of b1 = (*--> 0) * (signature A) & the ResultSort of b1 = (dom (signature A)) --> 0 & the carrier of b2 = {0} & the carrier' of b2 = dom (signature A) & the Arity of b2 = (*--> 0) * (signature A) & the ResultSort of b2 = (dom (signature A)) --> 0 holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines MSSign MSUALG_1:def_8_:_
 for A being Universal_Algebra
for b2 being trivial non void strict segmental ManySortedSign holds
( b2 = MSSign A iff ( the carrier of b2 = {0} & the carrier' of b2 = dom (signature A) & the Arity of b2 = (*--> 0) * (signature A) & the ResultSort of b2 = (dom (signature A)) --> 0 ) );

registration
let A be Universal_Algebra;
cluster MSSign A ->  trivial non void 1 -element strict segmental ;
coherence
 MSSign A is 1 -element
proof
 the carrier of (MSSign A) = {0} by Def8;
hence  the carrier of (MSSign A) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;

definition
let A be Universal_Algebra;
func MSSorts A ->  V5() ManySortedSet of the carrier of (MSSign A) equals :: MSUALG_1:def 9
0 .--> the carrier of A;
coherence
 0 .--> the carrier of A is V5() ManySortedSet of the carrier of (MSSign A)
proof
set M = {0} --> the carrier of A;
 the carrier of (MSSign A) = {0} by Def8;
then reconsider M = {0} --> the carrier of A as ManySortedSet of the carrier of (MSSign A) ;
 M is V5() ;
hence  0 .--> the carrier of A is V5() ManySortedSet of the carrier of (MSSign A) ; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines MSSorts MSUALG_1:def_9_:_
 for A being Universal_Algebra holds MSSorts A = 0 .--> the carrier of A;

definition
let A be Universal_Algebra;
func MSCharact A ->  ManySortedFunction of ((MSSorts A) #) * the Arity of (MSSign A),(MSSorts A) * the ResultSort of (MSSign A) equals :: MSUALG_1:def 10
 the charact of A;
coherence
 the charact of A is ManySortedFunction of ((MSSorts A) #) * the Arity of (MSSign A),(MSSorts A) * the ResultSort of (MSSign A)
proof
A1: the ResultSort of (MSSign A) = (dom (signature A)) --> 0 by Def8;
reconsider OS = the carrier' of (MSSign A) as non empty set ;
reconsider DO = ((MSSorts A) #) * the Arity of (MSSign A), RO = (MSSorts A) * the ResultSort of (MSSign A) as ManySortedSet of OS ;
A2: the carrier' of (MSSign A) = dom (signature A) by Def8;
 len (signature A) = len the charact of A by UNIALG_1:def_4;
then A3: dom the charact of A = OS by A2, FINSEQ_3:29;
then reconsider O = the charact of A as ManySortedSet of OS by PARTFUN1:def_2, RELAT_1:def_18;
A4: the Arity of (MSSign A) = (*--> 0) * (signature A) by Def8;
reconsider O = O as ManySortedFunction of OS ;
A5: the carrier of (MSSign A) = {0} by Def8;
 O is ManySortedFunction of DO,RO
proof
set D = the carrier of A;
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in OS or O . i is Element of K10(K11((DO . i),(RO . i))) )
reconsider M = 0 .--> the carrier of A as ManySortedSet of {0} ;
A6: 0 in {0} by TARSKI:def_1;
assume A7: i in OS ; ::_thesis: O . i is Element of K10(K11((DO . i),(RO . i)))
then reconsider n = i as Nat by A2;
reconsider h = O . n as non empty homogeneous quasi_total PartFunc of ( the carrier of A *), the carrier of A by A3, A7, MARGREL1:def_24, UNIALG_1:1;
 n in dom ((dom (signature A)) --> 0) by A2, A7, FUNCOP_1:13;
then RO . i = (MSSorts A) . (((dom (signature A)) --> 0) . n) by A1, FUNCT_1:13
.= ({0} --> the carrier of A) . 0 by A2, A7, FUNCOP_1:7
.= the carrier of A by A6, FUNCOP_1:7 ;
then A8: rng h c= RO . i by RELAT_1:def_19;
reconsider o = i as Element of OS by A7;
DO . i = ((((MSSorts A) #) * (*--> 0)) * (signature A)) . n by A4, RELAT_1:36
.= ((M #) * (*--> 0)) . ((signature A) . n) by A5, A2, A7, FUNCT_1:13
.= ((M #) * (*--> 0)) . (arity h) by A2, A7, UNIALG_1:def_4
.= Funcs ((Seg (arity h)), the carrier of A) by FINSEQ_2:145
.= dom (O . o) by Th3 ;
hence  O . i is Element of K10(K11((DO . i),(RO . i))) by A8, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
hence  the charact of A is ManySortedFunction of ((MSSorts A) #) * the Arity of (MSSign A),(MSSorts A) * the ResultSort of (MSSign A) ; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines MSCharact MSUALG_1:def_10_:_
 for A being Universal_Algebra holds MSCharact A = the charact of A;

definition
let A be Universal_Algebra;
func MSAlg A ->  strict MSAlgebra over MSSign A equals :: MSUALG_1:def 11
 MSAlgebra(# (MSSorts A),(MSCharact A) #);
correctness
coherence
MSAlgebra(# (MSSorts A),(MSCharact A) #) is strict MSAlgebra over MSSign A;
;
end;

:: deftheorem  defines MSAlg MSUALG_1:def_11_:_
 for A being Universal_Algebra holds MSAlg A = MSAlgebra(# (MSSorts A),(MSCharact A) #);

registration
let A be Universal_Algebra;
cluster MSAlg A ->  strict non-empty ;
coherence
 MSAlg A is non-empty
proof
thus  the Sorts of (MSAlg A) is V5() ; :: according to MSUALG_1:def_3 ::_thesis: verum
end;
end;

definition
let MS be 1 -element ManySortedSign ;
let A be MSAlgebra over MS;
func the_sort_of A ->  set  means :Def12: :: MSUALG_1:def 12
it is Component of the Sorts of A;
existence
 ex b1 being set st b1 is Component of the Sorts of A
proof
set c = the Component of the Sorts of A;
take  the Component of the Sorts of A ; ::_thesis: the Component of the Sorts of A is Component of the Sorts of A
thus  the Component of the Sorts of A is Component of the Sorts of A ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st b1 is Component of the Sorts of A & b2 is Component of the Sorts of A holds
b1 = b2 by Th5;
end;

:: deftheorem Def12 defines the_sort_of MSUALG_1:def_12_:_
 for MS being 1 -element ManySortedSign
for A being MSAlgebra over MS
for b3 being set holds
( b3 = the_sort_of A iff b3 is Component of the Sorts of A );

registration
let MS be 1 -element ManySortedSign ;
let A be non-empty MSAlgebra over MS;
cluster the_sort_of A ->  non empty ;
coherence
 not the_sort_of A is empty
proof
 the_sort_of A is Component of the Sorts of A by Def12;
hence  not the_sort_of A is empty ; ::_thesis: verum
end;
end;

theorem Th6: :: MSUALG_1:6
for MS being non void 1 -element segmental ManySortedSign
for i being OperSymbol of MS
for A being non-empty MSAlgebra over MS holds Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A)
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for i being OperSymbol of MS
for A being non-empty MSAlgebra over MS holds Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A)
let i be OperSymbol of MS; ::_thesis: for A being non-empty MSAlgebra over MS holds Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A)
let A be non-empty MSAlgebra over MS; ::_thesis: Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A)
set m = len (the_arity_of i);
 dom the Arity of MS = the carrier' of MS by FUNCT_2:def_1;
then A1: Args (i,A) = ( the Sorts of A #) . ( the Arity of MS . i) by FUNCT_1:13
.= product ( the Sorts of A * (the_arity_of i)) by FINSEQ_2:def_5 ;
A2: rng (the_arity_of i) c= the carrier of MS by FINSEQ_1:def_4;
then  rng (the_arity_of i) c= dom the Sorts of A by PARTFUN1:def_2;
then A3: dom ( the Sorts of A * (the_arity_of i)) = dom (the_arity_of i) by RELAT_1:27;
A4: ex n being Nat st dom (the_arity_of i) = Seg n by FINSEQ_1:def_2;
thus  Args (i,A) c= (len (the_arity_of i)) -tuples_on (the_sort_of A) :: according to XBOOLE_0:def_10 ::_thesis: (len (the_arity_of i)) -tuples_on (the_sort_of A) c= Args (i,A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Args (i,A) or x in (len (the_arity_of i)) -tuples_on (the_sort_of A) )
assume  x in Args (i,A) ; ::_thesis: x in (len (the_arity_of i)) -tuples_on (the_sort_of A)
then consider g being Function such that
A5: x = g and
A6: dom g = dom ( the Sorts of A * (the_arity_of i)) and
A7: for j being set st j in dom ( the Sorts of A * (the_arity_of i)) holds
g . j in ( the Sorts of A * (the_arity_of i)) . j by A1, CARD_3:def_5;
reconsider p = g as FinSequence by A4, A3, A6, FINSEQ_1:def_2;
 rng p c= the_sort_of A
proof
let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in rng p or j in the_sort_of A )
assume  j in rng p ; ::_thesis: j in the_sort_of A
then consider u being set  such that
A8: u in dom g and
A9: p . u = j by FUNCT_1:def_3;
 (the_arity_of i) . u in rng (the_arity_of i) by A3, A6, A8, FUNCT_1:def_3;
then A10: the Sorts of A . ((the_arity_of i) . u) is Component of the Sorts of A by A2, PBOOLE:139;
 g . u in ( the Sorts of A * (the_arity_of i)) . u by A6, A7, A8;
then  g . u in the Sorts of A . ((the_arity_of i) . u) by A3, A6, A8, FUNCT_1:13;
hence  j in the_sort_of A by A9, A10, Def12; ::_thesis: verum
end;
then A11: p is FinSequence of the_sort_of A by FINSEQ_1:def_4;
 len p = len (the_arity_of i) by A3, A6, FINSEQ_3:29;
then  x is Element of (len (the_arity_of i)) -tuples_on (the_sort_of A) by A5, A11, FINSEQ_2:92;
hence  x in (len (the_arity_of i)) -tuples_on (the_sort_of A) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (len (the_arity_of i)) -tuples_on (the_sort_of A) or x in Args (i,A) )
assume  x in (len (the_arity_of i)) -tuples_on (the_sort_of A) ; ::_thesis: x in Args (i,A)
then  x in Funcs ((Seg (len (the_arity_of i))),(the_sort_of A)) by FINSEQ_2:93;
then consider g being Function such that
A12: x = g and
A13: dom g = Seg (len (the_arity_of i)) and
A14: rng g c= the_sort_of A by FUNCT_2:def_2;
A15: dom g = dom ( the Sorts of A * (the_arity_of i)) by A3, A13, FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(_the_Sorts_of_A_*_(the_arity_of_i))_holds_
g_._x_in_(_the_Sorts_of_A_*_(the_arity_of_i))_._x
let x be set ; ::_thesis: ( x in dom ( the Sorts of A * (the_arity_of i)) implies g . x in ( the Sorts of A * (the_arity_of i)) . x )
assume A16: x in dom ( the Sorts of A * (the_arity_of i)) ; ::_thesis: g . x in ( the Sorts of A * (the_arity_of i)) . x
then  (the_arity_of i) . x in rng (the_arity_of i) by A3, FUNCT_1:def_3;
then A17: the Sorts of A . ((the_arity_of i) . x) is Component of the Sorts of A by A2, PBOOLE:139;
 g . x in rng g by A15, A16, FUNCT_1:def_3;
then  g . x in the_sort_of A by A14;
then  g . x in the Sorts of A . ((the_arity_of i) . x) by A17, Def12;
hence  g . x in ( the Sorts of A * (the_arity_of i)) . x by A3, A16, FUNCT_1:13; ::_thesis: verum
end;
hence  x in Args (i,A) by A1, A12, A15, CARD_3:9; ::_thesis: verum
end;

theorem Th7: :: MSUALG_1:7
for MS being non void 1 -element segmental ManySortedSign
for i being OperSymbol of MS
for A being non-empty MSAlgebra over MS holds Args (i,A) c= (the_sort_of A) *
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for i being OperSymbol of MS
for A being non-empty MSAlgebra over MS holds Args (i,A) c= (the_sort_of A) *
let i be OperSymbol of MS; ::_thesis: for A being non-empty MSAlgebra over MS holds Args (i,A) c= (the_sort_of A) *
let A be non-empty MSAlgebra over MS; ::_thesis: Args (i,A) c= (the_sort_of A) *
 Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A) by Th6;
hence  Args (i,A) c= (the_sort_of A) * by FINSEQ_2:142; ::_thesis: verum
end;

theorem Th8: :: MSUALG_1:8
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS holds the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
proof
let MS be non void 1 -element segmental ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over MS holds the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
let A be non-empty MSAlgebra over MS; ::_thesis: the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
A1: dom the Charact of A = the carrier' of MS by PARTFUN1:def_2;
 ex n being Element of NAT st the carrier' of MS = Seg n
proof
consider n being Nat such that
A2: the carrier' of MS = Seg n by Def7;
 n in NAT by ORDINAL1:def_12;
hence  ex n being Element of NAT st the carrier' of MS = Seg n by A2; ::_thesis: verum
end;
then reconsider f = the Charact of A as FinSequence by A1, FINSEQ_1:def_2;
 f is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
proof
let x be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not x in rng f or x in PFuncs (((the_sort_of A) *),(the_sort_of A)) )
assume  x in rng f ; ::_thesis: x in PFuncs (((the_sort_of A) *),(the_sort_of A))
then consider i being set  such that
A3: i in the carrier' of MS and
A4: f . i = x by A1, FUNCT_1:def_3;
reconsider i = i as OperSymbol of MS by A3;
A5: the Sorts of A . ( the ResultSort of MS . i) is Component of the Sorts of A by PBOOLE:139;
 dom the ResultSort of MS = the carrier' of MS by FUNCT_2:def_1;
then ( the Sorts of A * the ResultSort of MS) . i = the Sorts of A . ( the ResultSort of MS . i) by FUNCT_1:13
.= the_sort_of A by A5, Def12 ;
then A6: x is Function of (Args (i,A)),(the_sort_of A) by A4, PBOOLE:def_15;
 Args (i,A) c= (the_sort_of A) * by Th7;
then  x is PartFunc of ((the_sort_of A) *),(the_sort_of A) by A6, RELSET_1:7;
hence  x in PFuncs (((the_sort_of A) *),(the_sort_of A)) by PARTFUN1:45; ::_thesis: verum
end;
hence  the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A)) ; ::_thesis: verum
end;

definition
let MS be non void 1 -element segmental ManySortedSign ;
let A be non-empty MSAlgebra over MS;
func the_charact_of A ->  PFuncFinSequence of (the_sort_of A) equals :: MSUALG_1:def 13
 the Charact of A;
coherence
 the Charact of A is PFuncFinSequence of (the_sort_of A) by Th8;
end;

:: deftheorem  defines the_charact_of MSUALG_1:def_13_:_
 for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS holds the_charact_of A = the Charact of A;


definition
let MS be non void 1 -element segmental ManySortedSign ;
let A be non-empty MSAlgebra over MS;
func 1-Alg A ->  strict Universal_Algebra equals :: MSUALG_1:def 14
 UAStr(# (the_sort_of A),(the_charact_of A) #);
coherence
 UAStr(# (the_sort_of A),(the_charact_of A) #) is strict Universal_Algebra
proof
A1: the_charact_of A is quasi_total
proof
let n be Nat; :: according to MARGREL1:def_24 ::_thesis: for b1 being Element of K10(K11(((the_sort_of A) *),(the_sort_of A))) holds
( not n in dom (the_charact_of A) or not b1 = (the_charact_of A) . n or b1 is quasi_total )
let h be PartFunc of ((the_sort_of A) *),(the_sort_of A); ::_thesis: ( not n in dom (the_charact_of A) or not h = (the_charact_of A) . n or h is quasi_total )
assume that
A2: n in dom (the_charact_of A) and
A3: h = (the_charact_of A) . n ; ::_thesis: h is quasi_total
reconsider o = n as OperSymbol of MS by A2, PARTFUN1:def_2;
let x be FinSequence of the_sort_of A; :: according to MARGREL1:def_22 ::_thesis: for b1 being FinSequence of the_sort_of A holds
( not len x = len b1 or not x in dom h or b1 in dom h )
let y be FinSequence of the_sort_of A; ::_thesis: ( not len x = len y or not x in dom h or y in dom h )
assume that
A4: len x = len y and
A5: x in dom h ; ::_thesis: y in dom h
A6: (( the Sorts of A #) * the Arity of MS) . o = Args (o,A) ;
 h is Function of ((( the Sorts of A #) * the Arity of MS) . o),(( the Sorts of A * the ResultSort of MS) . o) by A3, PBOOLE:def_15;
then A7: dom h = (( the Sorts of A #) * the Arity of MS) . o by FUNCT_2:def_1
.= (len (the_arity_of o)) -tuples_on (the_sort_of A) by A6, Th6 ;
then  len y = len (the_arity_of o) by A4, A5, CARD_1:def_7;
then  y is Element of dom h by A7, FINSEQ_2:92;
hence  y in dom h by A5; ::_thesis: verum
end;
A8: the_charact_of A is homogeneous
proof
let n be Nat; :: according to MARGREL1:def_23 ::_thesis: for b1 being Element of K10(K11(((the_sort_of A) *),(the_sort_of A))) holds
( not n in dom (the_charact_of A) or not b1 = (the_charact_of A) . n or b1 is homogeneous )
let h be PartFunc of ((the_sort_of A) *),(the_sort_of A); ::_thesis: ( not n in dom (the_charact_of A) or not h = (the_charact_of A) . n or h is homogeneous )
assume that
A9: n in dom (the_charact_of A) and
A10: h = (the_charact_of A) . n ; ::_thesis: h is homogeneous
reconsider o = n as OperSymbol of MS by A9, PARTFUN1:def_2;
thus  dom h is with_common_domain :: according to MARGREL1:def_21 ::_thesis: verum
proof
let x, y be FinSequence; :: according to MARGREL1:def_1 ::_thesis: ( not x in dom h or not y in dom h or len x = len y )
assume that
A11: x in dom h and
A12: y in dom h ; ::_thesis: len x = len y
A13: (( the Sorts of A #) * the Arity of MS) . o = Args (o,A) ;
 h is Function of ((( the Sorts of A #) * the Arity of MS) . o),(( the Sorts of A * the ResultSort of MS) . o) by A10, PBOOLE:def_15;
then A14: dom h = (( the Sorts of A #) * the Arity of MS) . o by FUNCT_2:def_1
.= (len (the_arity_of o)) -tuples_on (the_sort_of A) by A13, Th6 ;
hence  len x = len (the_arity_of o) by A11, CARD_1:def_7
.= len y by A12, A14, CARD_1:def_7 ;
::_thesis: verum
end;
end;
 the_charact_of A is non-empty
proof
let n be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not n in dom (the_charact_of A) or not (the_charact_of A) . n is empty )
assume  n in dom (the_charact_of A) ; ::_thesis: not (the_charact_of A) . n is empty
then reconsider o = n as OperSymbol of MS by PARTFUN1:def_2;
set h = (the_charact_of A) . n;
 (the_charact_of A) . n = Den (o,A) ;
hence  not (the_charact_of A) . n is empty ; ::_thesis: verum
end;
hence  UAStr(# (the_sort_of A),(the_charact_of A) #) is strict Universal_Algebra by A1, A8, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines 1-Alg MSUALG_1:def_14_:_
 for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS holds 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #);

theorem :: MSUALG_1:9
for A being strict Universal_Algebra holds A = 1-Alg (MSAlg A)
proof
let A be strict Universal_Algebra; ::_thesis: A = 1-Alg (MSAlg A)
 the carrier of A in { the carrier of A} by TARSKI:def_1;
then  the carrier of A in rng the Sorts of (MSAlg A) by FUNCOP_1:8;
hence  A = 1-Alg (MSAlg A) by Def12; ::_thesis: verum
end;

theorem :: MSUALG_1:10
for A being Universal_Algebra
for f being Function of (dom (signature A)),({0} *)
for z being Element of {0} st f = (*--> 0) * (signature A) holds
MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #)
proof
let A be Universal_Algebra; ::_thesis: for f being Function of (dom (signature A)),({0} *)
for z being Element of {0} st f = (*--> 0) * (signature A) holds
MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #)
let f be Function of (dom (signature A)),({0} *); ::_thesis: for z being Element of {0} st f = (*--> 0) * (signature A) holds
MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #)
let z be Element of {0}; ::_thesis: ( f = (*--> 0) * (signature A) implies MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) )
A1: ( the carrier' of (MSSign A) = dom (signature A) & the Arity of (MSSign A) = (*--> 0) * (signature A) ) by Def8;
 ( z = 0 & the carrier of (MSSign A) = {0} ) by Def8, TARSKI:def_1;
hence  ( f = (*--> 0) * (signature A) implies MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) ) by A1, Def8; ::_thesis: verum
end;