environ
vocabularies HIDDEN, XBOOLE_0, PBOOLE, STRUCT_0, MSUALG_1, SUBSET_1, PRALG_2, EQREL_1, FUNCT_1, CARD_3, RELAT_1, SETFAM_1, RLVECT_2, FUNCT_6, TARSKI, FUNCT_2, MARGREL1, UNIALG_2, FUNCT_5, FUNCOP_1, FINSEQ_4, PARTFUN1, MSUALG_3, MEMBER_1, ARYTM_3, WELLORD1, PRALG_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, STRUCT_0, FUNCT_2, FUNCOP_1, EQREL_1, FUNCT_5, FUNCT_6, CARD_3, PBOOLE, MSUALG_1, MSUALG_3, PRALG_2, PRALG_1, MSUALG_2;
definitions XBOOLE_0, FUNCT_1, MSUALG_3, PRALG_2, PBOOLE, TARSKI;
theorems PBOOLE, FUNCT_1, EQREL_1, PRALG_2, MSUALG_1, MSUALG_3, FUNCT_2, CARD_3, TARSKI, FUNCOP_1, MSUALG_2, PRALG_1, FUNCT_6, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, PARTFUN1;
schemes PBOOLE, MSSUBFAM;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, EQREL_1, PBOOLE, STRUCT_0, MSUALG_1, PRALG_2, MSUALG_3, CARD_3, RELSET_1;
constructors HIDDEN, EQREL_1, PRALG_1, PRALG_2, MSUALG_3, RELSET_1, FUNCT_5;
requirements HIDDEN, BOOLE, SUBSET;
equalities PRALG_2;
expansions XBOOLE_0, FUNCT_1, MSUALG_3, PBOOLE, TARSKI;
Lm1:
for f being Function
for x being set st x in product f holds
x is Function
;
definition
let I be non
empty set ;
let S be non
empty non
void ManySortedSign ;
let A be
MSAlgebra-Family of
I,
S;
let i be
Element of
I;
existence
ex b1 being ManySortedFunction of (product A),(A . i) st
for s being Element of S holds b1 . s = proj ((Carrier (A,s)),i)
uniqueness
for b1, b2 being ManySortedFunction of (product A),(A . i) st ( for s being Element of S holds b1 . s = proj ((Carrier (A,s)),i) ) & ( for s being Element of S holds b2 . s = proj ((Carrier (A,s)),i) ) holds
b1 = b2
end;