let it1, it2 be Polynomial of L; :: thesis: ( ex f being FinSequence of the carrier of () * ex s being FinSequence of L st
( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product () ) & ex f being FinSequence of the carrier of () * ex s being FinSequence of L st
( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it2 = Product () ) implies it1 = it2 )

given f1 being FinSequence of the carrier of () * , s1 being FinSequence of L such that A4: len f1 = card () and
A5: s1 = canFS () and
A6: for i being Element of NAT st i in dom f1 holds
f1 . i = fpoly_mult_root ((s1 /. i),(b . (s1 /. i))) and
A7: it1 = Product () ; :: thesis: ( for f being FinSequence of the carrier of () *
for s being FinSequence of L holds
( not len f = card () or not s = canFS () or ex i being Element of NAT st
( i in dom f & not f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) or not it2 = Product () ) or it1 = it2 )

given f2 being FinSequence of the carrier of () * , s2 being FinSequence of L such that A8: len f2 = card () and
A9: ( s2 = canFS () & ( for i being Element of NAT st i in dom f2 holds
f2 . i = fpoly_mult_root ((s2 /. i),(b . (s2 /. i))) ) ) and
A10: it2 = Product () ; :: thesis: it1 = it2
A11: dom f1 = dom f2 by ;
now :: thesis: for i being Nat st i in dom f1 holds
f1 . i = f2 . i
let i be Nat; :: thesis: ( i in dom f1 implies f1 . i = f2 . i )
assume A12: i in dom f1 ; :: thesis: f1 . i = f2 . i
hence f1 . i = fpoly_mult_root ((s1 /. i),(b . (s1 /. i))) by A6
.= f2 . i by A5, A9, A11, A12 ;
:: thesis: verum
end;
hence it1 = it2 by ; :: thesis: verum