theorem Th13: :: BASEL_2:13

for k, n being Nat
for R being commutative Ring
for z0, z1 being Element of R holds (<%z0,z1%> `^ n) . k = (n choose k) * ((z1 |^ k) * (z0 |^ (n -' k)))