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