set cS = canFS (support b);
set f = b * (canFS (support b));
A1: rng (b * (canFS (support b))) c= REAL ;
( support b c= dom b & rng (canFS (support b)) = support b ) by FUNCT_2:def 3, PRE_POLY:37;
then dom (b * (canFS (support b))) = dom (canFS (support b)) by RELAT_1:27;
then dom (b * (canFS (support b))) = Seg (len (canFS (support b))) by FINSEQ_1:def 3;
then b * (canFS (support b)) is FinSequence by FINSEQ_1:def 2;
then reconsider f = b * (canFS (support b)) as FinSequence of REAL by A1, FINSEQ_1:def 4;
take Sum f ; :: thesis: ex f being FinSequence of REAL st
( Sum f = Sum f & f = b * (canFS (support b)) )
thus ex f being FinSequence of REAL st
( Sum f = Sum f & f = b * (canFS (support b)) ) ; :: thesis: verum