rng (canFS (support b)) c= the carrier of L by XBOOLE_1:1;
then reconsider s = canFS (support b) as FinSequence of L by FINSEQ_1:def 4;
deffunc H₁( set ) -> FinSequence of (Polynom-Ring L) = fpoly_mult_root ((s /. $1),(b . (s /. $1)));
consider f being FinSequence such that
A1: len f = card (support b) and
A2: for k being Nat st k in dom f holds
f . k = H₁(k) from FINSEQ_1:sch 2();
rng f c= the carrier of (Polynom-Ring L) *

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider i being Nat such that
A3: ( i in dom f & f . i = x ) by FINSEQ_2:10;
x = H₁(i) by A2, A3;
hence x in the carrier of (Polynom-Ring L) * by FINSEQ_1:def 11; :: thesis:

end;

then reconsider f = f as FinSequence of the carrier of (Polynom-Ring L) * by FINSEQ_1:def 4;
reconsider it1 = Product (FlattenSeq f) as Polynomial of L by POLYNOM3:def 10;
take it1 ; :: thesis:
take f ; :: thesis:
take s ; :: thesis:
thus len f = card (support b) by A1; :: thesis:
thus s = canFS (support b) ; :: thesis:
thus for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A2; :: thesis:
thus it1 = Product (FlattenSeq f) ; :: thesis: