theorem Th12:
for
X,
Y being
set for
f1,
f2 being
Function of
X,
Y st ( for
x being
element st
x in X holds
f1 . x = f2 . x ) holds
f1 = f2
theorem
for
Q,
X,
Y 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 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
theorem Th63:
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 )