environ
vocabularies HIDDEN, PBOOLE, FINSEQ_1, RELAT_1, TARSKI, XBOOLE_0, MSUALG_1, SUBSET_1, STRUCT_0, EQREL_1, FUNCT_1, ORDERS_2, ORDERS_1, RELAT_2, NATTRA_1, MARGREL1, XXREAL_0, SEQM_3, CARD_5, CARD_LAR, FUNCOP_1, CARD_3, SETFAM_1, OSALG_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, ORDERS_1, FUNCT_2, EQREL_1, SETFAM_1, PARTFUN1, FINSEQ_1, FUNCOP_1, FINSEQ_2, CARD_3, PBOOLE, ORDERS_2, STRUCT_0, MSUALG_1, ORDERS_3;
definitions TARSKI;
theorems FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, PBOOLE, FUNCT_2, CARD_3, FINSEQ_3, FINSEQ_2, RELAT_1, RELSET_1, EQREL_1, ZFMISC_1, ORDERS_3, MSUALG_1, ORDERS_2, RELAT_2, GRFUNC_1, FUNCT_4, ORDERS_1, XTUPLE_0;
schemes FUNCT_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, EQREL_1, STRUCT_0, MSUALG_1, ORDERS_3, ORDINAL1, RELAT_1, PBOOLE, FINSEQ_1;
constructors HIDDEN, EQREL_1, ORDERS_3, RELSET_1, MSAFREE;
requirements HIDDEN, BOOLE, SUBSET;
equalities ;
expansions ;
Lm1:
for I being set
for f being ManySortedSet of I
for p being FinSequence of I holds
( dom (f * p) = dom p & len (f * p) = len p )
theorem Th1:
for
A,
O being non
empty set for
R being
Order of
A for
Ol being
Equivalence_Relation of
O for
f being
Function of
O,
(A *) for
g being
Function of
O,
A holds
( not
OverloadedRSSign(#
A,
R,
O,
Ol,
f,
g #) is
empty & not
OverloadedRSSign(#
A,
R,
O,
Ol,
f,
g #) is
void &
OverloadedRSSign(#
A,
R,
O,
Ol,
f,
g #) is
reflexive &
OverloadedRSSign(#
A,
R,
O,
Ol,
f,
g #) is
transitive &
OverloadedRSSign(#
A,
R,
O,
Ol,
f,
g #) is
antisymmetric )
registration
let A be non
empty set ;
let R be
Order of
A;
let O be non
empty set ;
let Ol be
Equivalence_Relation of
O;
let f be
Function of
O,
(A *);
let g be
Function of
O,
A;
coherence
( OverloadedRSSign(# A,R,O,Ol,f,g #) is strict & not OverloadedRSSign(# A,R,O,Ol,f,g #) is empty & OverloadedRSSign(# A,R,O,Ol,f,g #) is reflexive & OverloadedRSSign(# A,R,O,Ol,f,g #) is transitive & OverloadedRSSign(# A,R,O,Ol,f,g #) is antisymmetric )
by Th1;
end;
definition
let S be
OrderSortedSign;
let z be non
empty set ;
let z1 be
Element of
z;
existence
ex b1 being strict OSAlgebra of S st
( the Sorts of b1 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b1) = (Args (o,b1)) --> z1 ) )
uniqueness
for b1, b2 being strict OSAlgebra of S st the Sorts of b1 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b1) = (Args (o,b1)) --> z1 ) & the Sorts of b2 = ConstOSSet (S,z) & ( for o being OperSymbol of S holds Den (o,b2) = (Args (o,b2)) --> z1 ) holds
b1 = b2
end;
:: constant -> order-sorted ManySortedSet of R