let R be non degenerated comRing; :: thesis: for f, g being Element of (Formal-Series (1,R)) holds (BSFSeri R) . (f + g) = ((BSFSeri R) . f) + ((BSFSeri R) . g)
let f, g be Element of (Formal-Series (1,R)); :: thesis: (BSFSeri R) . (f + g) = ((BSFSeri R) . f) + ((BSFSeri R) . g)
consider f1 being Series of 1,R such that
A1: ( f1 = f & (BSFSeri R) . f = f1 * NBag1 ) by Def4;
consider g1 being Series of 1,R such that
A2: ( g1 = g & (BSFSeri R) . g = g1 * NBag1 ) by Def4;
consider fg1 being Series of 1,R such that
A3: ( fg1 = f + g & (BSFSeri R) . (f + g) = fg1 * NBag1 ) by Def4;
A4: fg1 = f1 + g1 by A1, A2, A3, Def3;
(BSFSeri R) . (f + g) = (f1 * NBag1) + (g1 * NBag1) by A3, A4, Th26
.= ((BSFSeri R) . f) + ((BSFSeri R) . g) by A1, A2, POLYALG1:def 2 ;
hence (BSFSeri R) . (f + g) = ((BSFSeri R) . f) + ((BSFSeri R) . g) ; :: thesis: verum