environ
vocabularies HIDDEN, RELAT_1, XBOOLE_0, ZFMISC_1, SUBSET_1, TARSKI, SETFAM_1, FUNCT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1;
definitions TARSKI, XBOOLE_0, RELAT_1, SETFAM_1, ZFMISC_1;
theorems TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, XBOOLE_1, SUBSET_1, XTUPLE_0;
schemes TARSKI, XBOOLE_0;
registrations XBOOLE_0, RELAT_1, ZFMISC_1;
constructors HIDDEN, SETFAM_1, RELAT_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities RELAT_1;
expansions TARSKI, XBOOLE_0, RELAT_1, ZFMISC_1;
Lm1:
for X being set
for f, g1, g2 being Function st rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X holds
g1 = g2