environ
vocabularies HIDDEN, TARSKI, XBOOLE_0, FUNCT_1, RELAT_1, SUBSET_1, FINSUB_1, BINOP_1, FINSET_1, FUNCOP_1, SETWISEO;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, FINSUB_1, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1;
definitions BINOP_1, TARSKI;
theorems FINSUB_1, ZFMISC_1, SUBSET_1, BINOP_1, TARSKI, FUNCT_1, FUNCT_2, FUNCOP_1, ENUMSET1, RELAT_1, XBOOLE_0, XBOOLE_1;
schemes FINSET_1, FUNCT_2, BINOP_1, SUBSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, FINSUB_1, RELAT_1, FUNCT_3, ZFMISC_1;
constructors HIDDEN, ENUMSET1, PARTFUN1, BINOP_1, FUNCOP_1, FINSET_1, FINSUB_1, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities RELAT_1;
expansions BINOP_1, TARSKI;
Lm1:
for X, Y being non empty set
for f being Function of X,Y
for A being Element of Fin X holds f .: A is Element of Fin Y
by FINSUB_1:def 5;
Lm2:
for D being non empty set
for X, P being set
for f being Function of X,D holds f .: P c= D
;