let
X
be
set
;
:: thesis:
for
m
being
Multiset
of
X
holds
(
dom
m
=
X
&
rng
m
c=
NAT
)
let
m
be
Multiset
of
X
;
:: thesis:
(
dom
m
=
X
&
rng
m
c=
NAT
)
m
is
Function
of
X
,
NAT
by
Th27
;
hence
(
dom
m
=
X
&
rng
m
c=
NAT
)
by
FUNCT_2:def 1
,
RELAT_1:def 19
;
:: thesis:
verum