set
v
= the
Element
of
X1
;
the
Element
of
X1
in
X1
by
A1
;
then
reconsider
v
= the
Element
of
X1
as
Element
of
X
;
v

v
=
0.
X
by
RLVECT_1:15
;
hence
0.
X
is
Element
of
X1
by
A1
,
RLSUB_1:3
;
:: thesis:
verum