begin
scheme
FuncEx1{
F1()
-> set ,
F2()
-> set ,
P1[
set ,
set ] } :
ex
f being
Function of
F1(),
F2() st
for
x being
set st
x in F1() holds
P1[
x,
f . x]
provided
A1:
for
x being
set st
x in F1() holds
ex
y being
set st
(
y in F2() &
P1[
x,
y] )
scheme
Lambda1{
F1()
-> set ,
F2()
-> set ,
F3(
set )
-> set } :
ex
f being
Function of
F1(),
F2() st
for
x being
set st
x in F1() holds
f . x = F3(
x)
provided
A1:
for
x being
set st
x in F1() holds
F3(
x)
in F2()
theorem
for
X,
Y being
set for
f being
Function of
X,
Y st ( for
y being
set st
y in Y holds
ex
x being
set st
(
x in X &
y = f . x ) ) holds
rng f = Y
theorem Th12:
for
X,
Y being
set for
f1,
f2 being
Function of
X,
Y st ( for
x being
set st
x in X holds
f1 . x = f2 . x ) holds
f1 = f2
theorem
for
X,
Y,
Q being
set for
f being
Function of
X,
Y st
Y <> {} holds
for
x being
set holds
(
x in f " Q iff (
x in X &
f . x in Q ) )
theorem Th63:
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
theorem Th64:
for
X,
Y,
P being
set for
f being
Function of
X,
Y for
y being
set st
y in f .: P holds
ex
x being
set st
(
x in X &
x in P &
y = f . x )
begin
scheme
Lambda1C{
F1()
-> set ,
F2()
-> set ,
P1[
set ],
F3(
set )
-> set ,
F4(
set )
-> set } :
ex
f being
Function of
F1(),
F2() st
for
x being
set st
x in F1() holds
( (
P1[
x] implies
f . x = F3(
x) ) & (
P1[
x] implies
f . x = F4(
x) ) )
provided
A1:
for
x being
set st
x in F1() holds
( (
P1[
x] implies
F3(
x)
in F2() ) & (
P1[
x] implies
F4(
x)
in F2() ) )
begin