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;

( 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

hence
it1 = it2
by A4, A7, A8, A10, FINSEQ_2:9; :: thesis: verumf1 . 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;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