let R be non degenerated comRing; :: thesis: for p, q being Element of (Polynom-Ring (1,R))
for f, g being Element of (Formal-Series (1,R)) st p = f & q = g holds
p + q = f + g
let p, q be Element of (Polynom-Ring (1,R)); :: thesis: for f, g being Element of (Formal-Series (1,R)) st p = f & q = g holds
p + q = f + g
let f, g be Element of (Formal-Series (1,R)); :: thesis: ( p = f & q = g implies p + q = f + g )
assume A1: ( p = f & q = g ) ; :: thesis: p + q = f + g
reconsider p0 = p, q0 = q as Polynomial of 1,R by POLYNOM1:def 11;
reconsider p1 = p0, q1 = q0 as Series of 1,R ;
p + q = p0 + q0 by POLYNOM1:def 11
.= f + g by A1, Def3 ;
hence p + q = f + g ; :: thesis: verum