for a, b being Real
for n being Nat holds
( (a,b) In_Power n = ((a,1) In_Power n) (#) ((1,b) Subnomial n) & (a,b) In_Power n = ((a,1) Subnomial n) (#) ((1,b) In_Power n) )