let R be non degenerated comRing; :: thesis: for f1, g1 being sequence of R holds (f1 + g1) * BagN1 = (f1 * BagN1) + (g1 * BagN1)
let f1, g1 be sequence of R; :: thesis: (f1 + g1) * BagN1 = (f1 * BagN1) + (g1 * BagN1)
A1: dom ((f1 + g1) * BagN1) = Bags 1 by FUNCT_2:def 1;
for o being object st o in dom ((f1 + g1) * BagN1) holds
((f1 + g1) * BagN1) . o = ((f1 * BagN1) + (g1 * BagN1)) . o

proof

let o be object ; :: thesis: ( o in dom ((f1 + g1) * BagN1) implies ((f1 + g1) * BagN1) . o = ((f1 * BagN1) + (g1 * BagN1)) . o )
assume o in dom ((f1 + g1) * BagN1) ; :: thesis: ((f1 + g1) * BagN1) . o = ((f1 * BagN1) + (g1 * BagN1)) . o
then reconsider b = o as Element of Bags 1 ;
A2: BagN1 . o = b . 0 by Def2;
reconsider s1 = f1 * BagN1 as Series of 1,R ;
reconsider t1 = g1 * BagN1 as Series of 1,R ;
A3: (f1 * BagN1) . b = f1 . (b . 0) by A2, FUNCT_2:15;
A4: (g1 * BagN1) . b = g1 . (b . 0) by A2, FUNCT_2:15;
((f1 + g1) * BagN1) . o = (f1 + g1) . (b . 0) by A2, FUNCT_2:15
.= (f1 . (b . 0)) + (g1 . (b . 0)) by NORMSP_1:def 2
.= ((f1 * BagN1) + (g1 * BagN1)) . o by A3, A4, POLYNOM1:15 ;
hence ((f1 + g1) * BagN1) . o = ((f1 * BagN1) + (g1 * BagN1)) . o ; :: thesis: verum

end;

hence (f1 + g1) * BagN1 = (f1 * BagN1) + (g1 * BagN1) by A1; :: thesis: verum