:: Basic Notation of Universal Algebra :: by Jaros{\l}aw Kotowicz, Beata Madras and Ma{\l}gorzata Korolkiewicz :: :: Received December 29, 1992 :: Copyright (c) 1992-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies FINSEQ_1, PARTFUN1, RELAT_1, NAT_1, FUNCT_2, TARSKI, XBOOLE_0, SUBSET_1, FUNCOP_1, FUNCT_1, STRUCT_0, NUMBERS, INCPROJ, XXREAL_0, UNIALG_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, RELAT_1, FUNCT_1, CARD_3, FINSEQ_1, FINSEQ_2, FUNCOP_1, STRUCT_0, PARTFUN1, XXREAL_0, MARGREL1; constructors PARTFUN1, FUNCOP_1, XXREAL_0, FINSEQ_2, STRUCT_0, CARD_3, MARGREL1; registrations ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1, XXREAL_0, STRUCT_0, FUNCT_1, FINSEQ_1, MARGREL1; requirements NUMERALS, BOOLE, SUBSET; begin reserve n for Nat; definition struct (1-sorted) UAStr (# carrier -> set, charact -> PFuncFinSequence of the carrier #); end; registration cluster non empty strict for UAStr; end; registration let D be non empty set, c be PFuncFinSequence of D; cluster UAStr (#D,c #) -> non empty; end; definition let IT be UAStr; attr IT is partial means :: UNIALG_1:def 1 the charact of IT is homogeneous; attr IT is quasi_total means :: UNIALG_1:def 2 the charact of IT is quasi_total; attr IT is non-empty means :: UNIALG_1:def 3 the charact of IT <> {} & the charact of IT is non-empty; end; registration cluster quasi_total partial non-empty strict non empty for UAStr; end; registration let U1 be partial UAStr; cluster the charact of U1 -> homogeneous; end; registration let U1 be quasi_total UAStr; cluster the charact of U1 -> quasi_total; end; registration let U1 be non-empty UAStr; cluster the charact of U1 -> non-empty non empty; end; definition mode Universal_Algebra is quasi_total partial non-empty non empty UAStr; end; reserve U1 for partial non-empty non empty UAStr; theorem :: UNIALG_1:1 n in dom the charact of U1 implies (the charact of U1).n is PartFunc of (the carrier of U1)*,the carrier of U1; definition let U1; func signature U1 -> FinSequence of NAT means :: UNIALG_1:def 4 len it = len the charact of U1 & for n st n in dom it holds for h be homogeneous non empty PartFunc of (the carrier of U1 )*,the carrier of U1 st h = (the charact of U1).n holds it.n = arity(h); end; begin :: Addenda :: from MSSUBLAT, 2007.05.13, A.T. registration let U0 be Universal_Algebra; cluster the charact of U0 -> Function-yielding; end;