let it1, it2 be Polynomial of L; :: thesis: ( ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root (s /. i),(b . (s /. i)) ) & it1 = Product (FlattenSeq f) ) & ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root (s /. i),(b . (s /. i)) ) & it2 = Product (FlattenSeq f) ) implies it1 = it2 )
given f1 being FinSequence of the carrier of (Polynom-Ring L) * , s1 being FinSequence of L such that A6: ( len f1 = card (support b) & s1 = canFS (support b) & ( for i being Element of NAT st i in dom f1 holds
f1 . i = fpoly_mult_root (s1 /. i),(b . (s1 /. i)) ) & it1 = Product (FlattenSeq f1) ) ; :: thesis: ( for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L holds
( not len f = card (support b) or not s = canFS (support b) 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 (FlattenSeq f) ) or it1 = it2 )
given f2 being FinSequence of the carrier of (Polynom-Ring L) * , s2 being FinSequence of L such that A7: ( len f2 = card (support b) & s2 = canFS (support b) & ( for i being Element of NAT st i in dom f2 holds
f2 . i = fpoly_mult_root (s2 /. i),(b . (s2 /. i)) ) & it2 = Product (FlattenSeq f2) ) ; :: thesis: it1 = it2
A8: dom f1 = dom f2 by A6, A7, FINSEQ_3:31;

now

let i be Nat; :: thesis: ( i in dom f1 implies f1 . i = f2 . i )
assume A10: 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 A6, A7, A8, A10 ;
:: thesis: verum

end;

hence it1 = it2 by A6, A7, FINSEQ_2:10; :: thesis: verum