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