theorem Th9: :: BASEL_2:9

for k, n being Nat
for R being commutative Ring
for z0, z1 being Element of R holds
( (<%z0,z1%> `^ 0) . 0 = 1. R & ( n > 0 implies (<%(0. R),z1%> `^ n) . n = z1 |^ n ) & ( k <> n implies (<%(0. R),z1%> `^ n) . k = 0. R ) )