thus
F
*
f
is
Function-yielding
:: thesis:
verum
proof
let
x
be
object
;
:: according to
FUNCOP_1:def 6
:: thesis:
(
x
in
dom
(
F
*
f
)
implies
(
F
*
f
)
.
x
is
Function
)
assume
x
in
dom
(
F
*
f
)
;
:: thesis:
(
F
*
f
)
.
x
is
Function
then
(
F
*
f
)
.
x
=
F
.
(
f
.
x
)
by
FUNCT_1:12
;
hence
(
F
*
f
)
.
x
is
Function
;
:: thesis:
verum
end;