reconsider
f
=
f
as
LinearOperator
of
X
,
Y
by
Def7
;
f
.
v
is
VECTOR
of
Y
;
hence
f
.
v
is
VECTOR
of
Y
;
:: thesis:
verum