set f = b * (SgmX (RelIncl n),(support b));
A1: dom b = n by PARTFUN1:def 4;
rng b c= NAT by VALUED_0:def 6;
then reconsider bb = b as Function of n,NAT by A1, FUNCT_2:4;
bb = b ;
then reconsider f = b * (SgmX (RelIncl n),(support b)) as FinSequence of NAT by FINSEQ_2:36;
reconsider x = Sum f as Element of NAT ;
take x ; :: thesis: ex f being FinSequence of NAT st
( x = Sum f & f = b * (SgmX (RelIncl n),(support b)) )
thus ex f being FinSequence of NAT st
( x = Sum f & f = b * (SgmX (RelIncl n),(support b)) ) ; :: thesis: verum