let R be non degenerated comRing; :: thesis: the carrier of (Polynom-Ring (1,R)) c= the carrier of (Formal-Series (1,R))
Polynom-Ring (1,R) is Subring of Formal-Series (1,R) by Th21;
hence the carrier of (Polynom-Ring (1,R)) c= the carrier of (Formal-Series (1,R)) by C0SP1:def 3; :: thesis: verum