let n be set ; :: thesis: for L being non empty addLoopStr
for p, q being Series of n,L
for x being bag of n holds (p + q) . x = (p . x) + (q . x)
let L be non empty addLoopStr ; :: thesis: for p, q being Series of n,L
for x being bag of n holds (p + q) . x = (p . x) + (q . x)
let p, q be Series of n,L; :: thesis: for x being bag of n holds (p + q) . x = (p . x) + (q . x)
let x be bag of n; :: thesis: (p + q) . x = (p . x) + (q . x)
A1: ( dom p = Bags n & dom q = Bags n ) by FUNCT_2:def 1;
A2: x in Bags n by PRE_POLY:def 12;
then A3: ( p /. x = p . x & q /. x = q . x ) by A1, PARTFUN1:def 6;
A4: dom (p + q) = (dom p) /\ (dom q) by VFUNCT_1:def 1;
hence (p + q) . x = (p + q) /. x by A1, A2, PARTFUN1:def 6
.= (p . x) + (q . x) by A1, A2, A3, A4, VFUNCT_1:def 1 ;
:: thesis: verum