rng (canFS ()) c= the carrier of L by XBOOLE_1:1;
then reconsider s = canFS () as FinSequence of L by FINSEQ_1:def 4;
deffunc H1( set ) -> FinSequence of () = fpoly_mult_root ((s /. \$1),(b . (s /. \$1)));
consider f being FinSequence such that
A1: len f = card () and
A2: for k being Nat st k in dom f holds
f . k = H1(k) from rng f c= the carrier of () *
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in the carrier of () * )
assume x in rng f ; :: thesis: x in the carrier of () *
then consider i being Nat such that
A3: ( i in dom f & f . i = x ) by FINSEQ_2:10;
x = H1(i) by A2, A3;
hence x in the carrier of () * by FINSEQ_1:def 11; :: thesis: verum
end;
then reconsider f = f as FinSequence of the carrier of () * by FINSEQ_1:def 4;
reconsider it1 = Product () as Polynomial of L by POLYNOM3:def 10;
take it1 ; :: thesis: ex f being FinSequence of the carrier of () * ex s being FinSequence of L st
( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product () )

take f ; :: thesis: ex s being FinSequence of L st
( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product () )

take s ; :: thesis: ( len f = card () & s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product () )

thus len f = card () by A1; :: thesis: ( s = canFS () & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) & it1 = Product () )

thus s = canFS () ; :: 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 () )

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 ()
thus it1 = Product () ; :: thesis: verum