set scmult = the Mult of V | [:INT,(a * V):];
[:INT,(a * V):] c= [:INT, the carrier of V:] by ZFMISC_1:96;
then [:INT,(a * V):] c= dom the Mult of V by FUNCT_2:def 1;
then A1: dom ( the Mult of V | [:INT,(a * V):]) = [:INT,(a * V):] by RELAT_1:62;
for z being object st z in [:INT,(a * V):] holds
( the Mult of V | [:INT,(a * V):]) . z in a * V

proof

let z be object ; :: thesis: ( z in [:INT,(a * V):] implies ( the Mult of V | [:INT,(a * V):]) . z in a * V )
assume A2: z in [:INT,(a * V):] ; :: thesis: ( the Mult of V | [:INT,(a * V):]) . z in a * V
consider x, y being object such that
A3: ( x in INT & y in a * V & z = [x,y] ) by A2, ZFMISC_1:def 2;
reconsider i = x as Element of INT by A3;
consider v being Element of V such that
A4: y = a * v by A3;
( the Mult of V | [:INT,(a * V):]) . z = i * (a * v) by A2, A3, A4, FUNCT_1:49
.= (i * a) * v by ZMODUL01:def 4
.= a * (i * v) by ZMODUL01:def 4 ;
hence ( the Mult of V | [:INT,(a * V):]) . z in a * V ; :: thesis: verum

end;

hence the Mult of V | [:INT,(a * V):] is Function of [:INT,(a * V):],(a * V) by A1, FUNCT_2:3; :: thesis: verum