for D being non empty set
for f, g being FinSequence of PFuncs (D,REAL) st f,g are_fiberwise_equipotent holds
Sum f = Sum g