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_{1}( 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_{1}(k)
from FINSEQ_1:sch 2();

rng f c= the carrier of (Polynom-Ring L) *

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

then reconsider s = canFS (support b) as FinSequence of L by FINSEQ_1:def 4;

deffunc H

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

rng f c= the carrier of (Polynom-Ring L) *

proof

then reconsider f = f as FinSequence of the carrier of (Polynom-Ring L) * by FINSEQ_1:def 4;
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_{1}(i)
by A2, A3;

hence x in the carrier of (Polynom-Ring L) * by FINSEQ_1:def 11; :: thesis: verum

end;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

hence x in the carrier of (Polynom-Ring L) * by FINSEQ_1:def 11; :: thesis: verum

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