let a, b be Real; :: thesis: for n being Nat holds (a,b) Subnomial n = ((a,1) Subnomial n) (#) ((1,b) Subnomial n)
let n be Nat; :: thesis: (a,b) Subnomial n = ((a,1) Subnomial n) (#) ((1,b) Subnomial n)
((a * 1),(b * 1)) Subnomial n = ((a,1) Subnomial n) (#) ((1,b) Subnomial n) by ST;
hence (a,b) Subnomial n = ((a,1) Subnomial n) (#) ((1,b) Subnomial n) ; :: thesis: verum