let x, y be Element of L; :: according to VECTSP_1:def 26 :: thesis: for b₁, b₂ being Element of the carrier of (Formal-Series L) holds
( x * (b₁ + b₂) = (x * b₁) + (x * b₂) & (x + y) * b₁ = (x * b₁) + (y * b₁) & (x * y) * b₁ = x * (y * b₁) & (1. L) * b₁ = b₁ )
reconsider x' = x, y' = y as Element of L ;
let v, w be Element of (Formal-Series L); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. L) * v = v )
reconsider p = v, q = w as sequence of L by Def2;
A1: x * v = x * p by Def2;
A2: x * w = x * q by Def2;
A3: y * v = y * p by Def2;
reconsider k = v + w as Element of (Formal-Series L) ;
reconsider r = k as sequence of L by Def2;
x * k = x * r by Def2;
hence x * (v + w) = x * (p + q) by Def2
.= (x' * p) + (x' * q) by Th6
.= (x * v) + (x * w) by A1, A2, Def2 ;
:: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. L) * v = v )
thus (x + y) * v = (x' + y') * p by Def2
.= (x' * p) + (y' * p) by Th7
.= (x * v) + (y * v) by A1, A3, Def2 ; :: thesis: ( (x * y) * v = x * (y * v) & (1. L) * v = v )
thus (x * y) * v = (x' * y') * p by Def2
.= x' * (y' * p) by Th8
.= x * (y * v) by A3, Def2 ; :: thesis: (1. L) * v = v
thus (1. L) * v = (1. L) * p by Def2
.= v by Th9 ; :: thesis: verum