theorem
Th1
:
:: BOOLMARK:1
for
A
,
B
being non
empty
set
for
f
being
Function
of
A
,
B
for
C
being
Subset
of
A
for
v
being
Element
of
B
holds
f
+*
(
C
-->
v
)
is
Function
of
A
,
B