let n be Nat; :: thesis: (bseq 0) . n = 1
thus (bseq 0) . n = (n choose 0) * (n ^ (- 0)) by Def2
.= 1 * (n ^ (- 0)) by NEWTON:19
.= 1 by POWER:24 ; :: thesis: verum