environ
vocabularies HIDDEN, RELAT_1, XBOOLE_0, PARTFUN1, FUNCT_1, TARSKI, SUBSET_1, ZFMISC_1, RELAT_2, MCART_1, SETFAM_1, FUNCT_2, GROUP_9;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1;
definitions TARSKI, XBOOLE_0, PARTFUN1, FUNCT_1;
theorems TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, PARTFUN1, GRFUNC_1, RELSET_1, SUBSET_1, XBOOLE_0, XBOOLE_1, RELAT_2, MCART_1, SETFAM_1, XTUPLE_0;
schemes FUNCT_1, PARTFUN1, XBOOLE_0, RELSET_1, SUBSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1, GRFUNC_1, ZFMISC_1;
constructors HIDDEN, RELAT_2, PARTFUN1, MCART_1, SETFAM_1, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities PARTFUN1, SUBSET_1;
expansions TARSKI, XBOOLE_0, PARTFUN1, FUNCT_1;
theorem Th12:
for
X,
Y being
set for
f1,
f2 being
Function of
X,
Y st ( for
x being
object st
x in X holds
f1 . x = f2 . x ) holds
f1 = f2
theorem Th62:
for
X,
Y being
set for
f1,
f2 being
Function of
X,
Y st ( for
x being
Element of
X holds
f1 . x = f2 . x ) holds
f1 = f2
scheme
Lambda1C{
F1()
-> set ,
F2()
-> set ,
P1[
object ],
F3(
object )
-> object ,
F4(
object )
-> object } :
ex
f being
Function of
F1(),
F2() st
for
x being
object st
x in F1() holds
( (
P1[
x] implies
f . x = F3(
x) ) & (
P1[
x] implies
f . x = F4(
x) ) )
provided
A1:
for
x being
object st
x in F1() holds
( (
P1[
x] implies
F3(
x)
in F2() ) & (
P1[
x] implies
F4(
x)
in F2() ) )