set F = Formal-Series (n,L);
thus Formal-Series (n,L) is vector-distributive :: thesis: ( Formal-Series (n,L) is scalar-distributive & Formal-Series (n,L) is scalar-associative & Formal-Series (n,L) is scalar-unital )

proof

let x be Element of L; :: according to VECTSP_1:def 13 :: thesis: for b₁, b₂ being Element of the carrier of (Formal-Series (n,L)) holds x * (b₁ + b₂) = (x * b₁) + (x * b₂)
let v, w be Element of (Formal-Series (n,L)); :: thesis: x * (v + w) = (x * v) + (x * w)
reconsider p = v, q = w as Series of n,L by Def3;
reconsider x9 = x as Element of L ;
reconsider k = v + w as Element of (Formal-Series (n,L)) ;
A1: x * v = x * p by Def3;
reconsider r = k as Series of n,L by Def3;
A2: x * w = x * q by Def3;
x * k = x * r by Def3;
hence x * (v + w) = x * (p + q) by Def3
.= (x * p) + (x * q) by Th16
.= (x * v) + (x * w) by A1, A2, Def3 ;
:: thesis: verum

end;

thus Formal-Series (n,L) is scalar-distributive :: thesis: ( Formal-Series (n,L) is scalar-associative & Formal-Series (n,L) is scalar-unital )

proof

let x, y be Element of L; :: according to VECTSP_1:def 14 :: thesis: for b₁ being Element of the carrier of (Formal-Series (n,L)) holds (x + y) * b₁ = (x * b₁) + (y * b₁)
let v be Element of (Formal-Series (n,L)); :: thesis: (x + y) * v = (x * v) + (y * v)
reconsider p = v as Series of n,L by Def3;
reconsider x9 = x, y9 = y as Element of L ;
A3: x * v = x * p by Def3;
A4: y * v = y * p by Def3;
thus (x + y) * v = (x9 + y9) * p by Def3
.= (x9 * p) + (y9 * p) by Th17
.= (x * v) + (y * v) by A3, A4, Def3 ; :: thesis: verum

end;

thus Formal-Series (n,L) is scalar-associative :: thesis: Formal-Series (n,L) is scalar-unital

proof

let x, y be Element of L; :: according to VECTSP_1:def 15 :: thesis: for b₁ being Element of the carrier of (Formal-Series (n,L)) holds (x * y) * b₁ = x * (y * b₁)
let v be Element of (Formal-Series (n,L)); :: thesis: (x * y) * v = x * (y * v)
reconsider p = v as Series of n,L by Def3;
reconsider x9 = x, y9 = y as Element of L ;
A5: y * v = y * p by Def3;
thus (x * y) * v = (x9 * y9) * p by Def3
.= x9 * (y9 * p) by Th18
.= x * (y * v) by A5, Def3 ; :: thesis: verum

end;

let v be Element of (Formal-Series (n,L)); :: according to VECTSP_1:def 16 :: thesis: (1. L) * v = v
reconsider p = v as Series of n,L by Def3;
thus (1. L) * v = (1. L) * p by Def3
.= v by Th19 ; :: thesis: verum