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

( 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

hence
w1 = w2
by FUNCT_2:63; :: thesis: verum
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 A38, A41, Th7;

hence w1 . c = w2 . c by A37, A38, A39, A40, A41, A42, Th7; :: thesis: verum

end;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 A38, A41, Th7;

hence w1 . c = w2 . c by A37, A38, A39, A40, A41, A42, Th7; :: thesis: verum