let x be Element of (Formal-Series L); :: according to VECTSP_1:def 6 :: thesis: ( x * (1. (Formal-Series L)) = x & (1. (Formal-Series L)) * x = x )
set F = Formal-Series L;
1. (Formal-Series L) = 1_. L by Def2;
hence ( x * (1. (Formal-Series L)) = x & (1. (Formal-Series L)) * x = x ) by Lm1; :: thesis: verum