let n be Element of NAT ; :: thesis: (bseq 0 ) . n = 1
thus (bseq 0 ) . n = (n choose 0 ) * (n ^ (- 0 )) by Def2
.= 1 * (n ^ (- 0 )) by NEWTON:29
.= 1 by POWER:29 ; :: thesis: verum