begin
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;
begin
begin
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