reconsider
j
= 1 as
Element
of
REAL
by
XREAL_0:def 1
;
take
NAT
-->
j
;
:: thesis:
(
(
NAT
-->
j
)
.
0
=
1 & ( for
n
being
Element
of
NAT
holds
(
NAT
-->
j
)
.
n
>=
0
) )
thus
(
(
NAT
-->
j
)
.
0
=
1 & ( for
n
being
Element
of
NAT
holds
(
NAT
-->
j
)
.
n
>=
0
) )
by
FUNCOP_1:7
;
:: thesis:
verum