let w1, w2 be Polynomial of (o1 +^ o2),L; ( ( 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 )
; w1 = w2
for c being Element of Bags (o1 +^ o2) holds w1 . c = w2 . c
proof
let c be
Element of
Bags (o1 +^ o2);
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;
verum
end;
hence
w1 = w2
by FUNCT_2:63; verum