let w1, w2 be Polynomial of (o1 +^ o2),L; :: thesis: ( ( for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & w1 . b = Q1 . b2 ) ) & ( for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & w2 . b = Q1 . b2 ) ) implies w1 = w2 )

assume that
A35: for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & w1 . b = Q1 . b2 ) and
A36: for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & w2 . b = Q1 . b2 ) ; :: thesis: w1 = w2
for c being Element of Bags (o1 +^ o2) holds w1 . c = w2 . c
proof
let c be Element of Bags (o1 +^ o2); :: thesis: w1 . c = w2 . c
consider c1 being Element of Bags o1, c2 being Element of Bags o2, Q1 being Polynomial of o2,L such that
A37: Q1 = P . c1 and
A38: c = c1 +^ c2 and
A39: w1 . c = Q1 . c2 by A35;
consider d1 being Element of Bags o1, d2 being Element of Bags o2, S1 being Polynomial of o2,L such that
A40: S1 = P . d1 and
A41: c = d1 +^ d2 and
A42: w2 . c = S1 . d2 by A36;
c2 = d2 by ;
hence w1 . c = w2 . c by A37, A38, A39, A40, A41, A42, Th7; :: thesis: verum
end;
hence w1 = w2 by FUNCT_2:63; :: thesis: verum