A1
:
dom
(
fire
C
)
=
Funcs
(
P
,
NAT
)
by
Th26
;
A2
:
rng
(
fire
C
)
c=
Funcs
(
P
,
NAT
)
by
Th26
;
m
in
dom
(
fire
C
)
by
A1
,
FUNCT_2:8
;
then
[
m
,
(
(
fire
C
)
.
m
)
]
in
fire
C
by
FUNCT_1:def 2
;
then
(
fire
C
)
.
m
in
rng
(
fire
C
)
by
XTUPLE_0:def 13
;
hence
(
fire
C
)
.
m
is
marking
of
P
by
A2
,
FUNCT_2:66
;
:: thesis:
verum