set E = S;
set F = R;
set P = VecSp (S,R);
A1: R is Subring of S by Def1;
then A2: the carrier of R c= the carrier of S by C0SP1:def 3;

hereby :: according to VECTSP_1:def 14 :: thesis: ( VecSp (S,R) is scalar-associative & VecSp (S,R) is scalar-unital & VecSp (S,R) is vector-distributive )

let x, y be Element of R; :: thesis: for v being Element of (VecSp (S,R)) holds (x + y) * v = (x * v) + (y * v)
let v be Element of (VecSp (S,R)); :: thesis: (x + y) * v = (x * v) + (y * v)
reconsider a = x, b = y, c = v as Element of S by A2, Def5;
A3: (a + b) * c = (a * c) + (b * c) by VECTSP_1:def 3;
( x * v = a * c & y * v = b * c ) by Lm3;
then (x * v) + (y * v) = (a * c) + (b * c) by Def5;
hence (x + y) * v = (x * v) + (y * v) by A3, Lm3, Lm4; :: thesis: verum

end;

hereby :: according to VECTSP_1:def 15 :: thesis: ( VecSp (S,R) is scalar-unital & VecSp (S,R) is vector-distributive )

let x, y be Element of R; :: thesis: for v being Element of (VecSp (S,R)) holds (x * y) * v = x * (y * v)
let v be Element of (VecSp (S,R)); :: thesis: (x * y) * v = x * (y * v)
reconsider a = x, b = y, c = v as Element of S by A2, Def5;
A4: (a * b) * c = a * (b * c) by GROUP_1:def 3;
A5: (a * b) * c = (x * y) * v by Lm3, Lm5;
b * c = y * v by Lm3;
hence (x * y) * v = x * (y * v) by A4, A5, Lm3; :: thesis: verum

end;

hereby :: according to VECTSP_1:def 16 :: thesis: VecSp (S,R) is vector-distributive

let v be Element of (VecSp (S,R)); :: thesis: (1. R) * v = v
reconsider c = v as Element of S by Def5;
A6: 1. R = 1. S by C0SP1:def 3, A1;
(1. S) * c = c ;
hence (1. R) * v = v by Lm3, A6; :: thesis: verum

end;

hereby :: according to VECTSP_1:def 13 :: thesis: verum

let x be Element of R; :: thesis: for v, w being Element of (VecSp (S,R)) holds x * (v + w) = (x * v) + (x * w)
let v, w be Element of (VecSp (S,R)); :: thesis: x * (v + w) = (x * v) + (x * w)
reconsider a = x, b = v, c = w as Element of S by A2, Def5;
A7: a * (b + c) = (a * b) + (a * c) by VECTSP_1:def 2;
b + c = v + w by Def5;
then A8: a * (b + c) = x * (v + w) by Lm3;
( a * b = x * v & a * c = x * w ) by Lm3;
hence x * (v + w) = (x * v) + (x * w) by A7, A8, Def5; :: thesis: verum

end;