consider f being FinSequence of COMPLEX such that
A1: Product b = Product f and
A2: f = b * (canFS (support b)) by Def5;
( rng b c= NAT & rng f c= rng b ) by A2, RELAT_1:26, VALUED_0:def 6;
then rng f c= NAT ;
then reconsider g = f as FinSequence of NAT by FINSEQ_1:def 4;
Product g in NAT ;
hence Product b is Element of NAT by A1; :: thesis: verum