set F = f | W;
A1: dom (f | W) = the carrier of W by FUNCT_2:def 1;

A2: now :: thesis: for a being Scalar of K
for v1 being Vector of W holds (f | W) . (a * v1) = a * ((f | W) . v1)

let a be Scalar of K; :: thesis: for v1 being Vector of W holds (f | W) . (a * v1) = a * ((f | W) . v1)
let v1 be Vector of W; :: thesis: (f | W) . (a * v1) = a * ((f | W) . v1)
reconsider v2 = v1 as Vector of V1 by VECTSP_4:10;
a * v1 = a * v2 by VECTSP_4:14;
hence (f | W) . (a * v1) = f . (a * v2) by A1, FUNCT_1:47
.= a * (f . v2) by MOD_2:def 2
.= a * ((f | W) . v1) by A1, FUNCT_1:47 ;
:: thesis: verum

end;

now :: thesis: for v1, w1 being Vector of W holds (f | W) . (v1 + w1) = ((f | W) . v1) + ((f | W) . w1)

let v1, w1 be Vector of W; :: thesis: (f | W) . (v1 + w1) = ((f | W) . v1) + ((f | W) . w1)
reconsider v2 = v1, w2 = w1 as Vector of V1 by VECTSP_4:10;
v1 + w1 = v2 + w2 by VECTSP_4:13;
hence (f | W) . (v1 + w1) = f . (v2 + w2) by A1, FUNCT_1:47
.= (f . v2) + (f . w2) by VECTSP_1:def 20
.= ((f | W) . v1) + (f . w2) by A1, FUNCT_1:47
.= ((f | W) . v1) + ((f | W) . w1) by A1, FUNCT_1:47 ;
:: thesis: verum

end;

then ( f | W is additive & f | W is homogeneous ) by A2, MOD_2:def 2;
hence f | W is linear-transformation of W,V2 ; :: thesis: verum