set I = the carrier of R;
set scmult = the lmult of V | [: the carrier of R,(a * V):];
[: the carrier of R,(a * V):] c= [: the carrier of R, the carrier of V:]
by ZFMISC_1:96;
then
[: the carrier of R,(a * V):] c= dom the lmult of V
by FUNCT_2:def 1;
then A1:
dom ( the lmult of V | [: the carrier of R,(a * V):]) = [: the carrier of R,(a * V):]
by RELAT_1:62;
for z being object st z in [: the carrier of R,(a * V):] holds
( the lmult of V | [: the carrier of R,(a * V):]) . z in a * V
proof
let z be
object ;
( z in [: the carrier of R,(a * V):] implies ( the lmult of V | [: the carrier of R,(a * V):]) . z in a * V )
assume A2:
z in [: the carrier of R,(a * V):]
;
( the lmult of V | [: the carrier of R,(a * V):]) . z in a * V
consider x,
y being
object such that A3:
(
x in the
carrier of
R &
y in a * V &
z = [x,y] )
by A2, ZFMISC_1:def 2;
reconsider i =
x as
Element of
R by A3;
consider v being
Element of
V such that A4:
y = a * v
by A3;
( the lmult of V | [: the carrier of R,(a * V):]) . z =
i * (a * v)
by A2, A3, A4, FUNCT_1:49
.=
(i * a) * v
by VECTSP_1:def 16
.=
(a * i) * v
.=
a * (i * v)
by VECTSP_1:def 16
;
hence
( the lmult of V | [: the carrier of R,(a * V):]) . z in a * V
;
verum
end;
hence
the lmult of V | [: the carrier of R,(a * V):] is Function of [: the carrier of R,(a * V):],(a * V)
by A1, FUNCT_2:3; verum