let n be set ; :: thesis: for L being non empty addLoopStr
for p, q, r being Series of n,L st ( for x being bag of n holds r . x = (p . x) + (q . x) ) holds
r = p + q
let L be non empty addLoopStr ; :: thesis: for p, q, r being Series of n,L st ( for x being bag of n holds r . x = (p . x) + (q . x) ) holds
r = p + q
let p, q, r be Series of n,L; :: thesis: ( ( for x being bag of n holds r . x = (p . x) + (q . x) ) implies r = p + q )
assume A1: for x being bag of n holds r . x = (p . x) + (q . x) ; :: thesis: r = p + q
let x be Element of Bags n; :: according to FUNCT_2:def 9 :: thesis: r . x = (p + q) . x
A2: dom (p + q) = Bags n by FUNCT_2:def 1;
then A3: (p + q) /. x = (p + q) . x by PARTFUN1:def 8;
( dom p = Bags n & dom q = Bags n ) by FUNCT_2:def 1;
then A5: ( p /. x = p . x & q /. x = q . x ) by PARTFUN1:def 8;
thus r . x = (p . x) + (q . x) by A1
.= (p + q) . x by A2, A3, A5, VFUNCT_1:def 1 ; :: thesis: verum