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 A4: len f1 = card (support b) and
A5: s1 = canFS (support b) 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 (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 A8: len f2 = card (support b) and
A9: ( 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))) ) ) and
A10: it2 = Product (FlattenSeq f2) ; :: thesis: it1 = it2
A11: dom f1 = dom f2 by A4, A8, FINSEQ_3:29;
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 A4, A7, A8, A10, FINSEQ_2:9; :: thesis: verum