set F = Formal-Series L;

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

reconsider p = v as sequence of L by Def2;

thus (1. L) * v = (1. L) * p by Def2

.= v by Th9 ; :: thesis: verum

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

proof

thus
Formal-Series L is scalar-distributive
:: thesis: ( Formal-Series L is scalar-associative & Formal-Series L is scalar-unital )
let x be Element of L; :: according to VECTSP_1:def 13 :: thesis: for b_{1}, b_{2} being Element of the carrier of (Formal-Series L) holds x * (b_{1} + b_{2}) = (x * b_{1}) + (x * b_{2})

let v, w be Element of (Formal-Series L); :: thesis: x * (v + w) = (x * v) + (x * w)

reconsider p = v, q = w as sequence of L by Def2;

reconsider x9 = x as Element of L ;

reconsider k = v + w as Element of (Formal-Series L) ;

A1: x * v = x * p by Def2;

reconsider r = k as sequence of L by Def2;

A2: x * w = x * q by Def2;

x * k = x * r by Def2;

hence x * (v + w) = x * (p + q) by Def2

.= (x9 * p) + (x9 * q) by Th6

.= (x * v) + (x * w) by A1, A2, Def2 ;

:: thesis: verum

end;let v, w be Element of (Formal-Series L); :: thesis: x * (v + w) = (x * v) + (x * w)

reconsider p = v, q = w as sequence of L by Def2;

reconsider x9 = x as Element of L ;

reconsider k = v + w as Element of (Formal-Series L) ;

A1: x * v = x * p by Def2;

reconsider r = k as sequence of L by Def2;

A2: x * w = x * q by Def2;

x * k = x * r by Def2;

hence x * (v + w) = x * (p + q) by Def2

.= (x9 * p) + (x9 * q) by Th6

.= (x * v) + (x * w) by A1, A2, Def2 ;

:: thesis: verum

proof

thus
Formal-Series L is scalar-associative
:: thesis: Formal-Series L is scalar-unital
let x, y be Element of L; :: according to VECTSP_1:def 14 :: thesis: for b_{1} being Element of the carrier of (Formal-Series L) holds (x + y) * b_{1} = (x * b_{1}) + (y * b_{1})

let v be Element of (Formal-Series L); :: thesis: (x + y) * v = (x * v) + (y * v)

reconsider p = v as sequence of L by Def2;

reconsider x9 = x, y9 = y as Element of L ;

A3: x * v = x * p by Def2;

A4: y * v = y * p by Def2;

thus (x + y) * v = (x9 + y9) * p by Def2

.= (x9 * p) + (y9 * p) by Th7

.= (x * v) + (y * v) by A3, A4, Def2 ; :: thesis: verum

end;let v be Element of (Formal-Series L); :: thesis: (x + y) * v = (x * v) + (y * v)

reconsider p = v as sequence of L by Def2;

reconsider x9 = x, y9 = y as Element of L ;

A3: x * v = x * p by Def2;

A4: y * v = y * p by Def2;

thus (x + y) * v = (x9 + y9) * p by Def2

.= (x9 * p) + (y9 * p) by Th7

.= (x * v) + (y * v) by A3, A4, Def2 ; :: thesis: verum

proof

let v be Element of (Formal-Series L); :: according to VECTSP_1:def 16 :: thesis: (1. L) * v = v
let x, y be Element of L; :: according to VECTSP_1:def 15 :: thesis: for b_{1} being Element of the carrier of (Formal-Series L) holds (x * y) * b_{1} = x * (y * b_{1})

let v be Element of (Formal-Series L); :: thesis: (x * y) * v = x * (y * v)

reconsider p = v as sequence of L by Def2;

reconsider x9 = x, y9 = y as Element of L ;

A5: y * v = y * p by Def2;

thus (x * y) * v = (x9 * y9) * p by Def2

.= x9 * (y9 * p) by Th8

.= x * (y * v) by A5, Def2 ; :: thesis: verum

end;let v be Element of (Formal-Series L); :: thesis: (x * y) * v = x * (y * v)

reconsider p = v as sequence of L by Def2;

reconsider x9 = x, y9 = y as Element of L ;

A5: y * v = y * p by Def2;

thus (x * y) * v = (x9 * y9) * p by Def2

.= x9 * (y9 * p) by Th8

.= x * (y * v) by A5, Def2 ; :: thesis: verum

reconsider p = v as sequence of L by Def2;

thus (1. L) * v = (1. L) * p by Def2

.= v by Th9 ; :: thesis: verum