[
x
,
y
]
is
set
by
TARSKI:1
;
then
reconsider
z
=
[
x
,
y
]
as
Point
of
[:
E
,
F
:]
by
PRVECT_3:9
;
f
.
z
is
Point
of
G
;
hence
f
.
(
x
,
y
) is
Point
of
G
;
:: thesis:
verum