theorem SFE: :: NEWTON04:67
for n being Nat
for a, b being Real holds (a,b) Subnomial n,(b,a) Subnomial n are_fiberwise_equipotent