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: ( not x in rng f or x in the carrier of (Polynom-Ring L) * )
assume x in rng f ; :: thesis: x in the carrier of (Polynom-Ring L) *
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: verum

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: 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) )
take f ; :: thesis: 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) )
take s ; :: thesis: ( 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) )
thus len f = card (support b) by A1; :: thesis: ( 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) )
thus s = canFS (support b) ; :: thesis: ( ( 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) )
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: it1 = Product (FlattenSeq f)
thus it1 = Product (FlattenSeq f) ; :: thesis: verum