environ
vocabularies HIDDEN, FUNCT_1, TARSKI, RELAT_1, XBOOLE_0, SUBSET_1;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ENUMSET1, RELAT_1, FUNCT_1;
definitions RELAT_1, XBOOLE_0, FUNCT_1;
theorems TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_1, ENUMSET1, XTUPLE_0;
schemes ;
registrations FUNCT_1, RELAT_1;
constructors HIDDEN, TARSKI, SUBSET_1, FUNCT_1, ENUMSET1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0;
expansions RELAT_1, FUNCT_1;
Lm1:
for x, y being object
for f, h being Function st (rng f) /\ (rng h) = {} & x in dom f & y in dom h holds
f . x <> h . y
Lm2:
for x, x1, y, y1 being object st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
Lm3:
for x being object
for f, g, h being Function st h = f \/ g holds
( x in dom h iff ( x in dom f or x in dom g ) )