consider
a
being
Vector
of
V
such that
A2
:
a
<>
0.
V
by
A1
;
take
<:
a
:>
;
:: thesis:
ex
a
being
Vector
of
V
st
(
a
<>
0.
V
&
<:
a
:>
=
<:
a
:>
)
thus
ex
a
being
Vector
of
V
st
(
a
<>
0.
V
&
<:
a
:>
=
<:
a
:>
)
by
A2
;
:: thesis:
verum