:: Basic Notation of Universal Algebra
:: by Jaros{\l}aw Kotowicz, Beata Madras and Ma{\l}gorzata Korolkiewicz
::
:: Received December 29, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

definition
attrc1 is strict ;
struct UAStr  ->  1-sorted ;
aggrUAStr(# carrier, charact #) ->  UAStr ;
sel charact c1 ->  PFuncFinSequence of the carrier of c1;
end;

registration
cluster non empty strict for UAStr ;
existence
 ex b1 being UAStr st
( not b1 is empty & b1 is strict )
proofend;
end;

registration
let D be non empty set ;
let c be PFuncFinSequence of D;
cluster UAStr(# D,c #) ->  non empty ;
coherence
 not UAStr(# D,c #) is empty ;
end;

definition
let IT be UAStr ;
attrIT is partial  means :Def1: :: UNIALG_1:def 1
 the charact of IT is homogeneous ;
attrIT is quasi_total  means :Def2: :: UNIALG_1:def 2
 the charact of IT is quasi_total ;
attrIT is non-empty  means :Def3: :: UNIALG_1:def 3
( the charact of IT <> {} &amp; the charact of IT is non-empty );
end;

:: deftheorem Def1 defines partial UNIALG_1:def_1_:_
 for IT being UAStr holds
( IT is partial iff the charact of IT is homogeneous );

:: deftheorem Def2 defines quasi_total UNIALG_1:def_2_:_
 for IT being UAStr holds
( IT is quasi_total iff the charact of IT is quasi_total );

:: deftheorem Def3 defines non-empty UNIALG_1:def_3_:_
 for IT being UAStr holds
( IT is non-empty iff ( the charact of IT <> {} &amp; the charact of IT is non-empty ) );

registration
cluster non empty strict partial quasi_total non-empty for UAStr ;
existence
 ex b1 being UAStr st
( b1 is quasi_total &amp; b1 is partial &amp; b1 is non-empty &amp; b1 is strict &amp; not b1 is empty )
proofend;
end;

registration
let U1 be partial UAStr ;
cluster the charact of U1 ->  homogeneous ;
coherence
 the charact of U1 is homogeneous by Def1;
end;

registration
let U1 be quasi_total UAStr ;
cluster the charact of U1 ->  quasi_total ;
coherence
 the charact of U1 is quasi_total by Def2;
end;

registration
let U1 be non-empty UAStr ;
cluster the charact of U1 ->  non-empty non empty ;
coherence
 ( the charact of U1 is non-empty &amp; not the charact of U1 is empty ) by Def3;
end;

definition
mode Universal_Algebra is non empty partial quasi_total non-empty UAStr ;
end;

theorem Th1: :: UNIALG_1:1
for n being Nat
for U1 being non empty partial non-empty UAStr st n in dom the charact of U1 holds
the charact of U1 . n is PartFunc of ( the carrier of U1 *), the carrier of U1
proofend;

definition
let U1 be non empty partial non-empty UAStr ;
func signature U1 ->  FinSequence of NAT  means :: UNIALG_1:def 4
( len it = len the charact of U1 &amp; ( for n being Nat st n in dom it holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
it . n = arity h ) );
existence
 ex b1 being FinSequence of NAT st
( len b1 = len the charact of U1 &amp; ( for n being Nat st n in dom b1 holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
b1 . n = arity h ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of NAT st len b1 = len the charact of U1 &amp; ( for n being Nat st n in dom b1 holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
b1 . n = arity h ) &amp; len b2 = len the charact of U1 &amp; ( for n being Nat st n in dom b2 holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
b2 . n = arity h ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines signature UNIALG_1:def_4_:_
 for U1 being non empty partial non-empty UAStr
for b2 being FinSequence of NAT holds
( b2 = signature U1 iff ( len b2 = len the charact of U1 &amp; ( for n being Nat st n in dom b2 holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
b2 . n = arity h ) ) );

begin

:: from MSSUBLAT, 2007.05.13, A.T.
registration
let U0 be Universal_Algebra;
cluster the charact of U0 ->  Function-yielding ;
coherence
 the charact of U0 is Function-yielding ;
end;