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;

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;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

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;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

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;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

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;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