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

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