( support b c= dom b & dom b = the carrier of L ) by PARTFUN1:def 4, PRE_POLY:37;
then 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 set ; :: 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:11;
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 12;
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