let
V
,
A
be
set
;
:: thesis:
A
c=
Union
(
FNDSC
(
V
,
A
)
)
set
F
=
FNDSC
(
V
,
A
);
A1
:
A
=
(
FNDSC
(
V
,
A
)
)
.
0
by
Def3
;
dom
(
FNDSC
(
V
,
A
)
)
=
NAT
by
Def3
;
then
(
FNDSC
(
V
,
A
))
.
0
in
rng
(
FNDSC
(
V
,
A
)
)
by
FUNCT_1:def 3
;
hence
A
c=
Union
(
FNDSC
(
V
,
A
)
)
by
A1
,
ZFMISC_1:74
;
:: thesis:
verum