let it1, it2 be Series of n,L; :: thesis: ( ( for x being bag of holds it1 . x = (p . x) + (q . x) ) & ( for x being bag of holds it2 . x = (p . x) + (q . x) ) implies it1 = it2 )
assume that
A2: for x being bag of holds it1 . x = (p . x) + (q . x) and
A3: for x being bag of holds it2 . x = (p . x) + (q . x) ; :: thesis: it1 = it2

now

let x be Element of Bags n; :: thesis: it1 . x = it2 . x
reconsider x' = x as bag of ;
thus it1 . x = (p . x') + (q . x') by A2
.= it2 . x by A3 ; :: thesis: verum

end;

hence it1 = it2 by FUNCT_2:113; :: thesis: verum