environ
vocabularies HIDDEN, STRUCT_0, FUNCT_1, RELAT_1, XBOOLE_0, FUNCOP_1, SUBSET_1, MARGREL1, PBOOLE, CARD_1, NAT_1, UNIALG_1, FUNCT_2, PARTFUN1, FINSEQ_2, TARSKI, FINSEQ_1, NUMBERS, ZFMISC_1, CARD_3, MSUALG_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, PARTFUN1, FINSEQ_2, CARD_3, FUNCOP_1, PBOOLE, MARGREL1, UNIALG_1;
definitions TARSKI, FINSEQ_1, FUNCT_1, PBOOLE, STRUCT_0, XBOOLE_0, MARGREL1;
theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, UNIALG_1, PBOOLE, FUNCT_2, CARD_3, FINSEQ_3, FINSEQ_2, RELAT_1, RELSET_1, ORDINAL1, MARGREL1, CARD_1;
schemes ;
registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSEQ_2, RELAT_1, PBOOLE, STRUCT_0, UNIALG_1, FUNCT_2, CARD_1, ZFMISC_1, MARGREL1, FINSEQ_1;
constructors HIDDEN, CARD_3, PBOOLE, REALSET2, UNIALG_1, RELSET_1, MARGREL1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities XBOOLE_0, FUNCOP_1;
expansions STRUCT_0;
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
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 )