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

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

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; :: thesis: verum
let z be object ; :: thesis: ( 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):] ; :: thesis: ( 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 ; :: thesis: verum

end;assume A2: z in [: the carrier of R,(a * V):] ; :: thesis: ( 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 ; :: thesis: verum