let n be Nat; :: thesis: for a, b being Real holds (a,b) Subnomial n,(b,a) Subnomial n are_fiberwise_equipotent
let a, b be Real; :: thesis: (a,b) Subnomial n,(b,a) Subnomial n are_fiberwise_equipotent
(a,b) Subnomial n, Rev ((a,b) Subnomial n) are_fiberwise_equipotent by FFE;
hence (a,b) Subnomial n,(b,a) Subnomial n are_fiberwise_equipotent by SAB; :: thesis: verum