set cS = canFS (support b);
set f = b * (canFS (support b));
A1: support b c= dom b by POLYNOM1:41;
rng (canFS (support b)) = support b by FUNCT_2:def 3;
then dom (b * (canFS (support b))) = dom (canFS (support b)) by A1, RELAT_1:46;
then dom (b * (canFS (support b))) = Seg (len (canFS (support b))) by FINSEQ_1:def 3;
then A2: b * (canFS (support b)) is FinSequence by FINSEQ_1:def 2;
rng (b * (canFS (support b))) c= COMPLEX by VALUED_0:def 1;
then reconsider f = b * (canFS (support b)) as FinSequence of COMPLEX by A2, FINSEQ_1:def 4;
take S = Product f; :: thesis: ex f being FinSequence of COMPLEX st
( S = Product f & f = b * (canFS (support b)) )
thus ex f being FinSequence of COMPLEX st
( S = Product f & f = b * (canFS (support b)) ) ; :: thesis: verum