set f = b * (SgmX ((RelIncl n),(support b)));
A1: dom b = n by PARTFUN1:def 2;
rng b c= NAT by VALUED_0:def 6;
then reconsider bb = b as Function of n,NAT by A1, FUNCT_2:2;
bb = b ;
then reconsider f = b * (SgmX ((RelIncl n),(support b))) as FinSequence of NAT by FINSEQ_2:32;
reconsider x = Sum f as 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