for a being non empty FinSequence of REAL
for f being FinSequence of NAT
for j, b being Nat st (len f) + 1 <= len a & b <> j holds
SumBin (a,(f ^ <*b*>),{j}) = SumBin (a,f,{j}) by NF110;