let
X
be
set
;
:: thesis:
for
A
being
Subset
of
X
ex
F
being
sequence
of
(
bool
X
)
st
rng
F
=
{
A
}
let
A
be
Subset
of
X
;
:: thesis:
ex
F
being
sequence
of
(
bool
X
)
st
rng
F
=
{
A
}
take
NAT
-->
A
;
:: thesis:
rng
(
NAT
-->
A
)
=
{
A
}
thus
rng
(
NAT
-->
A
)
=
{
A
}
by
FUNCOP_1:8
;
:: thesis:
verum