[|
X
, the
Sorts
of
T
|]
.
a
=
[:
(
X
.
a
)
,
(
the
Sorts
of
T
.
a
)
:]
by
PBOOLE:def 16
;
then
(
dom
[|
X
, the
Sorts
of
T
|]
=
the
carrier
of
J
&
[
x
,
t
]
in
[|
X
, the
Sorts
of
T
|]
.
a
)
by
ZFMISC_1:87
,
PARTFUN1:def 2
;
hence
the
assignments
of
A
.
[
x
,
t
]
is
Algorithm
of
A
by
CARD_5:2
,
FUNCT_2:5
;
:: thesis:
verum