let R be Ring; :: thesis: for f, g being Series of 1,R holds (f + g) * NBag1 = (f * NBag1) + (g * NBag1)
let f, g be Series of 1,R; :: thesis: (f + g) * NBag1 = (f * NBag1) + (g * NBag1)
for o being object st o in NAT holds
((f + g) * NBag1) . o = ((f * NBag1) + (g * NBag1)) . o

proof

let o be object ; :: thesis: ( o in NAT implies ((f + g) * NBag1) . o = ((f * NBag1) + (g * NBag1)) . o )
assume A1: o in NAT ; :: thesis: ((f + g) * NBag1) . o = ((f * NBag1) + (g * NBag1)) . o
then reconsider m = o as Element of NAT ;
A2: NBag1 . o = 1 --> m by Def1;
reconsider b = NBag1 . o as Element of Bags 1 by A2, PRE_POLY:def 12;
A3: f . b = (f * NBag1) . m by FUNCT_2:15;
A4: g . b = (g * NBag1) . m by FUNCT_2:15;
((f + g) * NBag1) . o = (f + g) . b by A1, FUNCT_2:15
.= ((f * NBag1) . m) + ((g * NBag1) . m) by A3, A4, POLYNOM1:15
.= ((f * NBag1) + (g * NBag1)) . o by NORMSP_1:def 2 ;
hence ((f + g) * NBag1) . o = ((f * NBag1) + (g * NBag1)) . o ; :: thesis: verum

end;

hence (f + g) * NBag1 = (f * NBag1) + (g * NBag1) ; :: thesis: verum