consider
g
being
Function
such that
A1
:
f
=
g
and
A2
:
dom
g
=
X
and
A3
:
rng
g
c=
the
carrier
of
Y
by
FUNCT_2:def 2
;
f
.
x
in
rng
g
by
A1
,
A2
,
FUNCT_1:def 3
;
hence
f
.
x
is
VECTOR
of
Y
by
A3
;
:: thesis:
verum